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.

Contract inference consists in automatically computing contracts that formally describe the behaviour of program functions. Contracts are used in deductive verification, which is a method for verifying whether a system behaves according to a provided specification. The Saida plugin in Frama-C is a contract inference tool for C code. This thesis explores an extension to the Saida plugin which allows support for pointers and heap allocations. The goal is to evaluate to what extent model checking tools can be used to infer contracts for deductive verification of programs that use pointers and heap allocations. This is done by proposing a translation strategy to convert contracts containing heap expressions, generated by the model checker TriCera, into ACSL, a specification language used by Frama-C. An implementation of this translation is evaluated using a set of verification tasks. The results demonstrate that the inferred contracts are sucient to verify simple code samples, including features such as recursion, aliasing, and manipulation of heap-allocated structs. However, the results also reveal cases where the contracts are too weak, although more information could be extracted in the translation. It is concluded that model checking tools can infer contracts for deductive verification of programs with pointers and heap allocations, but currently to a limited extent. Several improvements to the translation strategy are proposed for future work. / Kontrakthärledning består i att automatiskt härleda kontrakt, vilka formellt beskriver funktioners beteende i program. Kontrakt används för deduktiv verifiering, vilket är en metod för att verifiera huruvida ett system beter sig enligt en given specifikation. Pluginet Saida i Frama-C är ett verktyg för kontrakthärledning för C-kod. Denna avhandling undersöker en vidareutveckling av Saida som möjliggör stöd för pekare och heap-allokeringar. Målet är att utvärdera i vilken utsträckning modellprovningsverktyg kan användas för att härleda kontrakt för deduktiv verifiering av program som använder pekare och heap-allokeringar. Detta görs genom att presentera en översättningsstrategi för att konvertera kontrakt som involverar heaputtryck, genererade av modellkontrollverktyget TriCera, till ACSL, vilket är ett specifikationsspråk som används av Frama-C. En implementation av denna översättning utvärderas med hjälp av en samling verifieringsproblem. Resultaten visar att de härledda kontrakten är tillräckliga för att verifiera enkla verifieringsproblem, med koncept som rekursion, aliasing och manipulation av heap-allokerade structs. Resultaten visar även fall då kontrakten är för svaga, men där mer information skulle kunna utvinnas i ¨översättningen. Slutsatsen dras att modellprovningsverktyg kan härleda kontrakt för deduktiv verifiering av program med pekare och heap-allokeringar, men för närvarande i begränsad utsträckning. Flera förbättringar av översättningsstrategin föreslås för framtida vidareutveckling.

This thesis explores synergies between deductive verification and model checking, by using the existing model checker TriCera to automatically infer specifications for the deductive verifier Frama-C. To accomplish this, a formal semantics is defined for a subset of ANSI C, extended with assume statements, called Csmall. Then, it is shown how a Hoare logic contract can be translated into statements in Csmall, and the defined formal semantics is used to prove that the translation is correct. Furthermore, it is shown that the translation can be applied also to a real specification language. This is done by defining a subset of ACSL, called ACSLsmall, and giving a formal semantics also for this. Lastly, two examples are provided showing that the theory developed in this thesis can be applied to automatically infer ACSL function contracts. / Den här avhandlingen studerar synergier mellan deduktiv verifikation och modelprovning, genom att använda Tricera, ett verktyg för modellprovning, för att automatiskt generera specifikationer för Frama-C, ett verktyg för deduktiv verifikation. Detta uppnås genom att definiera en formell semantik för en delmängd av ANSI-C, utökat med assume satser, som kallas förCsmall. Sedan visas hur kontrakt kan översättas till satser i Csmall samt att översättningen är korrekt. Därefter visas att översättningen också kan tillämpas på ett verkligt specifikationsspråk, genom att definiera en delmängd av ACSL, som kallas ACSLsmall, och definiera en formell semantik också för detta. Slutligen visas med två exempel hur teorin från uppsatsen kan appliceras för att automatiskt generera funktionskontrakt i ACSL.