Sökning: "Begränsad modellprovning"

Hittade 2 uppsatser innehållade orden Begränsad modellprovning.

1. 1. Automated Inference of ACSL Contracts for Programs with Heaps

   Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

   Författare :Oskar Söderberg; [2023]
   Nyckelord :Formal Verification; Contract Inference; Model Checking; Deductive Verification; Theory of Heaps; ACSL; Translation; Formell Verifiering; Kontrakth¨arledning; Modellprovning; Deduktiv Verifiering; Theory of Heaps; ACSL; Overs¨attning;

   Sammanfattning : 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. LÄS MER

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

   Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

   Författare :Gustav Ung; [2021]
   Nyckelord :Formal methods; Bounded Model Checking; Stateflow; SLDV; Formella metoder; Begränsad modellprovning; Stateflow; SLDV;

   Sammanfattning : 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. LÄS MER