Sökning: "Formal verification"

Visar resultat 1 - 5 av 105 avhandlingar innehållade orden Formal verification.

  1. 1. Formal Specification and Verification of Safety-Critical Software

    Författare :Daniel Larsson; [2006]
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; fault injection; fault tolerance; safety-critical; dependability; formal verification; Formal specification;

    Sammanfattning : This thesis is about formal specification and formal verification of software and consists of three different parts. In the first two parts, the formal specification language OCL is treated in two different contexts. The third part describes a technique for analysing the consequences of hardware faults as part of formal software verification. LÄS MER

  2. 2. Towards Formal Verification in a Component-based Reuse Methodology

    Detta är en avhandling från Institutionen för datavetenskap

    Författare :Daniel Karlsson; Petru Eles; Zebo Peng; [2003]
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Formal verification; Model checking; Petri net; Reuse; TECHNOLOGY Information technology Computer science; TEKNIKVETENSKAP Informationsteknik Datavetenskap;

    Sammanfattning : Embedded systems are becoming increasingly common in our everyday lives. As techonology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components (Intellectual Property blocks). LÄS MER

  3. 3. Automated Approaches for Formal Verification of Embedded Systems Artifacts

    Detta är en avhandling från Institutionen för datavetenskap

    Författare :Predrag Filipovikj; Cristina Seceleanu; Jim Woodcock; []
    Nyckelord :TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; embedded systems; Simulink; systems specifications; model-checking; formal verification; Computer Science; datavetenskap;

    Sammanfattning : Modern embedded software is so large and complex that creating the necessary artifacts, including system requirements specifications and design-time models, as well as assuring their correctness have become difficult to manage. One challenge stems from the high number and intricacy of system requirements that combine functional and possibly timing or other types of constraints, which make them hard to analyze. LÄS MER

  4. 4. Automatic Extraction of Program Models for Formal Software Verification

    Detta är en avhandling från Stockholm : KTH Royal Institute of Technology

    Författare :Pedro de Carvalho Gomes; Dilian Gurov; Einar Johnsen; [2015]
    Nyckelord :TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; Software Verification; Static Analysis; Program Models; Petri Nets; Compositional Verification; Concurrency; Datalogi; Computer Science;

    Sammanfattning : In this thesis we present a study of the generation of abstract program models from programs in real-world programming languages that are employed in the formal verification of software. The thesis is divided into three parts, which cover distinct types of software systems, programming languages, verification scenarios, program models and properties. LÄS MER

  5. 5. Formal Development of Safe and Secure Java Card Applets

    Detta är en avhandling från Stockholm : KTH Royal Institute of Technology

    Författare :Wojciech Mostowski; [2005]
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; object-oriented design; Java Card; formal verification; formal specification; dynamic logic;

    Sammanfattning : This thesis is concerned with formal development of Java Card applets. Java Card is a technology that provides a means to program smart cards with (a subset of) the Java language. In recent years Java Card technology gained great interest in the formal verification community. There are two reasons for this. LÄS MER