Talk "Hybrid system development in Event-B"

by Dominique Méry

Tue, 06 September 2022 at 10:00 am in Lipari, Italy

Joint work with: Zheng Cheng

Abstract: Hybrid systems are widely used in a variety of safety-critical applications. Therefore, it is vital to provide a high-level safety guarantee for their implementations. Based on the action system and the refinement methodology, researchers show how to model a safe time-triggered design in the Event-B language. It consists of system events that monitor the system state periodically and make appropriate actuation decisions for the system's safety. However, two crucial types of system events are missing in such design, i.e. sensing and actuation, which hinders the development of robust hybrid systems. In addition, Event-B is specialized in high-level system modeling. Its primitives are not expressive enough to naturally support refining system events into low-level software implementations. In this work, we propose a way to refine (by decomposition) the time-triggered design to introduce the missing system events, without complex high-level system modeling. Based on the decomposition, we identify which system events are implementable. Then, we define a translational approach to the B language. Our translational approach: 1) systematically modularizes a specified Event-B software operation from associated system events. 2) defines a verified translation to obtain a semantically equivalent correspondent in the B language for each modularized Event-B software operation. This translational approach allows us to reuse the primitives of B for refining system events down to implementations, and reuse the predicate transformers defined on the B primitives to reason for the correctness of refinements. It also ensures that the behaviors of the implementations obtained via refinements in B do not divert from the corresponding system events specified in Event-B.