Sökning: "Compositional Verification"

Visar resultat 1 - 5 av 11 avhandlingar innehållade orden Compositional Verification.

  1. 1. Algorithmic Verification Techniques for Mobile Code

    Författare :Irem Aktug; Dilian Gurov; Mads Dam; Ulfar Erlingsson; KTH; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Verification; Mobile Code Security; Reference Monitoring; Maximal Models; Compositional Verification; Theoretical computer science; Teoretisk datalogi;

    Sammanfattning : Modern computing platforms strive to support mobile code without putting system security at stake. These platforms can be viewed as open systems, as the mobile code adds new components to the running system. Establishing that such platforms function correctly can  be divided into two steps. LÄS MER

  3. 2. Procedure-Modular Verification of Temporal Safety Properties

    Författare :Siavash Soleimanifard; Dilian Gurov; Gerardo Schneider; KTH; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Modular Verification; Compositional Verification; Maximal Models; Model Checking; Temporal Properties;

    Sammanfattning : This thesis presents a fully automated technique for procedure-modular verification of control flow temporal safety properties. Procedure-modular verification is a natural instantiation of modular verification where modularity is achieved at the level of procedures. LÄS MER

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

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

    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. 4. Sound Modular Extraction of Control Flow Graphs from Java Bytecode

    Författare :Pedro de Carvalho Gomes; Dilian Gurov; Wolfgang Ahrendt; KTH; []
    Nyckelord :TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; Software Verification; Static Analysis; Program Models; Compositional Verification;

    Sammanfattning : Control flow graphs (CFGs) are abstract program models that preserve the control flow information. They have been widely utilized for many static analyses in the past decades. LÄS MER

  7. 5. Compositional Approaches in Supervisory Control with Application to Automatic Generation of Robot Interlocking Policies

    Författare :Hugo Flordal; Chalmers tekniska högskola; []
    Nyckelord :TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; NATURVETENSKAP; NATURAL SCIENCES; nonblocking; finite state automata; verification; controllability; Discrete event systems; model reduction; synthesis; interlocking; supervisory control;

    Sammanfattning : The work presented in this thesis concerns verification and synthesis in the Ramadge and Wonham supervisory control framework. Supervisory control constitutes a formal framework for the design of supervisors for discrete event systems. LÄS MER