Essays about: "Formal Verification"

Showing result 21 - 25 of 82 essays containing the words Formal Verification.

  1. 21. Formal verification of device driver monitors in HOL 4

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Tomas Möre; [2021]
    Keywords : ;

    Abstract : 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. READ MORE

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

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Gustav Ung; [2021]
    Keywords : Formal methods; Bounded Model Checking; Stateflow; SLDV; Formella metoder; Begränsad modellprovning; Stateflow; SLDV;

    Abstract : 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. READ MORE

  4. 23. Plant Model Generator from Digital Twin for Purpose of Formal Verification

    University essay from Luleå tekniska universitet/Institutionen för system- och rymdteknik

    Author : Johannes Håkansson; [2021]
    Keywords : Digital twin; Plant verification; Model checking; Functional properties;

    Abstract : 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. READ MORE

  5. 24. Proof-producing resolution of indirect jumps in the binary intermediate representation BIR

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Adrian Westerberg; [2021]
    Keywords : Formal verification; Binary analysis; Interactive theorem proving; Indirect jump resolution; Formell verifiering; Binär analys; Interaktiv teorembevisning; Indirekt hopp bestämning;

    Abstract : 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. READ MORE

  6. 25. Automatically Learning Register Automata from MATLAB Code : A case study in autonomous driving

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Marco Dei Rossi; [2021]
    Keywords : Automata learning; SL*; Register automata; RALib; Lateral State Manager; Automata learning; SL*; Register automata; RALib; LSM; Automata learning; SL*; Register automata; RALib; LSM;

    Abstract : 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. READ MORE