Research on the verification method of the Event-B model for the heterogeneous multi-core scheduling algorithm

It is well known that the logical verification for the operating system is very essential. Event-B, as a formal verification tool, is one of the most widely used methods for verifying programs at the operating system level. However, it lacks the precise time semantics expression that will make the representation of the behavioral logic complicated for verified scheduling process. To address this limitation, we proposes an EMPT (Event-B Multi-core Processor Time) model in rodin platform, which can represent the time semantics by using set mappings and operations. After that we apply it to the logical verification for the heterogeneous multicore scheduling algorithm (HEFT), and the results show that it can verify the accuracy of this algorithm.