Patterns for Modeling Task-Level Timing Constraints with Event-B

Specification and verification of timing properties is a critical but error-prone issue in the development of real-time systems. Event-B is a formalism with the aim of modeling and analyzing systems. But it does not directly support the modeling of timing properties. Several studies have extended Event-B to formalize timing properties. These works are mainly concerned with timing constraints between events without the consideration of task-level timing constraints. In this paper, we propose patterns for task-level timing constraints precedence and coincidence. Firstly, we introduce the pattern for task deadline that states timing properties within a task. Then patterns for precedence and coincidence are built on top of this one. Furthermore, we illustrate the application of proposed patterns through the formal development of an example. It shows that the patterns can be integrated with Event-B models smoothly by the refinement. Our patterns can be potentially applicable to a wide range of modeling safety critical real-time systems. Additionally, our work provides a reference for the specification of other task-level timing constraints, e.g., exclusion and sub-occurrence.