A Timed Automata based Automatic Framework for Verifying STL Properties of Simulink Models

Simulink has been widely used in model-based design and development. While we witness a growing demand on testing and verification for safety-critical systems, it remains a challenge to verify Simulink models, due largely to a lack of standardized formal semantics for Simulink. In this paper, we propose a comprehensive framework that allows us to automatically verify Simulink models. Our proposed framework is equipped with Signal Temporal Logic (STL) for system requirements specification and employs a formal method to translate Simulink models into UPPAAL timed automata, which can then be verified automatically by UPPAAL (against their STL specification). A novelty of our work is the integration of Simulink models with STL, allowing us to express and then verify complex time properties that may be found difficult by existing work. In our translation of Simulink models, we adopt symbolic execution to reduce the size of the translated automata that can produce accurate results. We also demonstrate the feasibility and effectiveness of the proposed framework via a case study of an autonomous driving system.