Implementation and evaluation of bounded invariant model checking for a subset of Stateflow

• Main Author: Ung, Gustav
• Format: Others
• Language: English
• Published: KTH, Skolan för elektroteknik och datavetenskap (EECS) 2021
• Subjects: Formal methods; Bounded Model Checking; Stateflow; SLDV; Formella metoder; Begränsad modellprovning; Computer Sciences; Datavetenskap (datalogi)
• Online Access: http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-301654

Stateflowmodels are used for describing logic and implementing state machines in modern safety-critical software. However, the complete Stateflowmodelling language is hard to formally define, therefore a subset relevant for industrial models has been developed in previous works. Proving that the execution of Stateflow models satisfies certain safety properties is intractable in general. However, bounded model checking (BMC) can be used to either prove that safety properties are satisfied up to a bounded execution depth, commonly referred to as the reachability diameter, or find a concrete counterexample. One particular safety property of interest is an invariant property. This thesis project contributes with the following. A bounded model checking tool based on symbolic execution has been developed and is called Stateflow Model Verification Tool (SMVT). This tool has been tested on synthetic models and industrial models. The performance of Stateflow Model Verification Tool (SMVT) has been measured, but not compared against the Simulink DesignVerifier (SLDV) due to licensing issues. The study has shown that many industrial models share a similar model structure. Furthermore, it has been shown that SMVT can perform well for several models. === Stateflow-modeller används för att beskriva logik and implementation av tillståndsmaskiner i modern säkerhetskritisk mjukvara. Det kompletta Stateflowspråket är väldigt komplext, och därför har forskare tidigare definierat en begränsad version av språket relevant för industriella modeller. Bevisning att exekvering av Stateflow-modeller måste uppfylla säkerhetsegenskaper, är svårlösligt rent generellt. Begränsad modellprovning kan användas antingen för att bevisa att säkerhetsegenskaper uppfylls till ett begränsat exekveringsdjup, eller för att hitta ett motexempel. En väldigt viktig säkerhetsegenskap kallas för invariant. Detta examensarbete bidrar med följande. En begränsad modellprövare baserad på symbolisk exekvering har utvecklats och kallas för SMVT. Detta verktyg har blivit testat på syntetiska modeller samt industriella modeller. Prestandan har blivit mätt, men på grund av Simulink Design Verifier (SLDV) licens har ingen jämförelse kunnat göras. Studien har visat att många industriella modeller delar samma modellstruktur. Vidare har det utvecklade verktyget SMVT visats prestera väl för flertalet modeller.