Special Session: A Model-Driven Design Tool for Modelling, Simulation and Assertion-Based Verification of Hybrid Automata

In a cyber-physical system (CPS), physical and digital components are deeply intertwined, making its design and verification a challenging process. To manage this complexity, hybrid automata are generally adopted to model CPS, allowing the representation of both its discrete and continuous behaviours, which are implemented in the digital and the physical parts. While some tools exist at the state of the art for either modelling or verifying hybrid automata, they present some drawbacks, specifically in terms of ease of use and lack of a unified tool that makes seamless the integration of design, simulation and verification steps. To fill in the gap, we present a new EDA tool for model-driven design and verification of hybrid automata. It does not require designers to learn domain-specific languages, as automatons are graphically modeled; furthermore, the tool integrates a simulation engine for analyzing the evolution of the automata and detecting design errors through the execution of checkers synthesized from Signal Temporal Logic (STL) assertions. The effectiveness of the proposed tool is demonstrated with a case study.