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

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, most of these formal methods express their semantics by reduction to timed automata or timed transition systems, and are associated with model-checking-based verification techniques. In this regard, 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, that 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, and also how the extended expressivity of first-order logic and set theory at the core of Event-B enables finer modelling.