Sökning: "Formell verifikation"

Hittade 5 uppsatser innehållade orden Formell verifikation.

  1. 1. Automated inference of ACSL function contracts using TriCera

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

    Författare :Jesper Amilon; [2021]
    Nyckelord :Formal Verification; Contract inference; Hoare Logic; Model Checking; Horn clauses; Formell verifikation; Kontraktgenerering; Formell semantik; Hoare logik; Modellprovning; Horn clauses;

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

  3. 2. Verifying Correctness of Contract Decompositions

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

    Författare :Gustav Hedengran; [2020]
    Nyckelord :;

    Sammanfattning : The importance of verification in safety critical systems is well known. However, due to the complexity of verification, the task of formally verifying large safety-critical systems might prove computationally infeasible in many cases. Compositional verification is a technique aimed at enabling verification of large safety-critical systems. LÄS MER

  4. 3. Verifying Temporal Properties Using Deductive Verifiers

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

    Författare :Jesper Amilon; Axel Lindeberg; [2019]
    Nyckelord :;

    Sammanfattning : Formal verification is an area of theoretical computer science where mathematical logic is used to prove that a program behaves in a certain way. With the methods in formal verification, you can prove that the program follows some given specification and thereby behaves in the desired way. The area is largely split up into two distinct parts. LÄS MER

  5. 4. Formal Verification of Hardware Peripheral with Security Property

    Kandidat-uppsats, KTH/Skolan för datavetenskap och kommunikation (CSC)

    Författare :Jonathan Yao Håkansson; Niklas Rosencrantz; [2017]
    Nyckelord :Formal Verification NuSMV JavaPathFinder Spin Promela CTL LTL DMA UART Model Checking Theorem Proving;

    Sammanfattning : One problem with computers is that the operating system automatically trusts any externallyconnected peripheral. This can result in abuse when a peripheral technically can violate the security model because the peripheral is trusted. Because of that the security is an important issue to look at. LÄS MER

  7. 5. Semi-Automated Formalization and Verification of Automotive Requirements using Simulink Design Verifier

    Master-uppsats, KTH/Maskinkonstruktion (Inst.)

    Författare :Rohit Agrawal; [2015]
    Nyckelord :;

    Sammanfattning : The complexity of embedded software in the automotive domain is ever-increasing due to increase in the no. of features aimed at providing more advanced solutions. This has greatly favored the incorporation of Model Based Design workflow in the software development lifecycle to handle complexities in different development phases. LÄS MER