Hybrid automata: from verification to implementation

Hybrid automata are an important formalism for modeling dynamical systems exhibiting mixed discrete–continuous behavior such as control systems and are amenable to formal verification. However, hybrid automata lack expressiveness compared to integrated model-based design frameworks such as the MathWorks’ Simulink/Stateflow (SlSf). In this paper, we propose a technique for correct-by-construction compositional design of cyber-physical systems (CPS) by embedding hybrid automata into SlSf models. Hybrid automata are first verified using verification tools such as SpaceEx and then automatically translated to embed the hybrid automata into SlSf models such that the properties verified are transferred and maintained in the translated SlSf model. The resultant SlSf model can then be used for automatic code generation and deployment to hardware, resulting in an implementation. The approach is implemented in a software tool building on the HyST model transformation tool for hybrid systems. We show the effectiveness of our approach on a CPS case study—a closed-loop buck converter—and validate the overall correct-by-construction methodology: from formal verification to implementation in hardware controlling an actual physical plant.