IPA: Reusing of Properties after Discretization of Hybrid Automata

When designing embedded systems, often the need arises to model systems having a mixed discrete and continuous behavior (i.e., hybrid systems) that cannot be characterized faithfully using either only discrete or only continuous MoCs (models of computation). Hybrid automata [1] have been proved to be a powerful MoC for the design and verification of hybrid systems, but their high-level of abstraction cannot take into account all the details of the typical HW/SW designs. For this reason, once the hybrid model of the system is proved to be correct, is still necessary to derive an implementable model of the hybrid system. Very few works in literature have focused on developing techniques for extracting a correct by construction HW/SW implementation from hybrid automata [2], [3]. Unfortunately, these approaches are able to refine, into a systematic way, only a subclass of hybrid automata, thus they allow to automatically implement only a small class of hybrid systems. For this reason, it is not uncommon to manually refine hybrid automata into their corresponding discrete (e.g., SystemC [4]) or (approximated) continuous implementations (e.g., SystemC-AMS [4], Matlab Simulink). In such a case the refined system must be verified again to guarantee its correctness. In this context, it would be valuable to reuse as much as possible properties defined for the verification of hybrid automata to reduce the need of an error prone and time consuming ex-novo property definitions. To the best of our knowledge the refinement of formal properties from the hybrid into the discrete domains is still an open problem. The proposed methodology aims to fill this gap.