Correct-by-Construction Design of Timed Systems in Event-B

Abstract

Real-time systems require the careful handling of timing aspects in their models. For critical applications, this entails the use of time-aware formal methods. Currently, such formal methods only account for timing and communication layers, excluding functional aspects. Thus, they are intended to be used as a posteriori analysis methods, on systems that have already been developed. In contrast, methods such as Event-B have been designed to build systems incrementally using a correct-by-construction approach, but are not equipped with the ability to express timing aspects and constraints. We propose a non-intrusive, tool-supported embedding of time and clocks in Event-B inspired by the features and semantics of timed automata. This enables the design of complex real-time systems while benefiting from the entire ecosystem and tooling support of the method. Refinement is extended to also take time into account, making it possible to design complex systems gradually in a correct-by-construction manner while integrating timing aspects from the top level. The embedding and associated methodology are illustrated on a case study, showcasing both how timed Event-B models may be derived from timed automata, how the extended expressivity of first-order logic and set theory at the core of Event-B enables finer modelling, and how timed refinement may be used to establish complex timing properties.