Formalizing hierarchical scheduling for refinement of real-time systems

The Event-B formalism offers a stepwise development approach for managing complexity in system design. However, the existing work that extends Event-B models with discrete timing properties inadequately represents the communication and competition between concurrent tasks in concurrent systems. In this paper, we present the semantics of the parameterized real-time trigger-response properties of Event-B models based on timing invariants. We show a method of syntactically encoding parameterized real-time trigger-response properties in Event-B machines. To capture the concurrency between tasks, we distinguish end-to-end timing properties and scheduler-based timing properties from the perspective of different system design phases. We model end-to-end timing properties as parameterized timing properties and scheduler-based timing properties as unparameterized timing properties. A nondeterministic queue-based scheduling framework is proposed to replace end-to-end timing properties with scheduler-based timing properties. Additional gluing invariants are provided for this refinement. To demonstrate the usability of the framework, we formalize a two-level hierarchical scheduling system with local resource sharing managed by a time-division multiplexing global scheduler and two alternative local schedulers refined by the nondeterministic queue-based scheduling policy. Models are proved using the Rodin tool