Sökning: "Formal Verification"
Visar resultat 21 - 25 av 84 uppsatser innehållade orden Formal Verification.
21. Formal verification of device driver monitors in HOL 4
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)Sammanfattning : As computer systems become more ubiquitous in society the negative consequences of security holes and bugs in software and hardware grow larger. In theory, the optimal way to ensure that no such possibilites exists is to conduct formal proofs that the system behaves as it should and that it is incapable of performing unintended side-effects. LÄS MER
22. Implementation and evaluation of bounded invariant model checking for a subset of Stateflow
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)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
23. Plant Model Generator from Digital Twin for Purpose of Formal Verification
Uppsats för yrkesexamina på avancerad nivå, Luleå tekniska universitet/Institutionen för system- och rymdteknikSammanfattning : This master thesis will cover a way to automatically generate a formal model for plant verification from plant traces. The solution will be developed from trace data, stemming from a model of a digital twin of a physical plant. LÄS MER
24. Proof-producing resolution of indirect jumps in the binary intermediate representation BIR
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)Sammanfattning : HolBA is a binary analysis library that can be used to formally verify binary programs using contracts. It is developed in the interactive theorem prover HOL4 to achieve a high degree of trust in verification, the result of verification is a machine-checked proof demonstrating its correctness. This thesis presents two proof-producing procedures. LÄS MER
25. Automatically Learning Register Automata from MATLAB Code : A case study in autonomous driving
Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)Sammanfattning : The successful verification of the behaviour of an Autonomous driving (AD) vehicle is fundamental for the commercialization of this new technology. Formal verification can be used to exhaustively verify the correctness of a system, but it requires a formal model to do so. LÄS MER