Sökning: "Formal verification"

Visar resultat 21 - 25 av 134 avhandlingar innehållade orden Formal verification.

  1. 21. INCREMENTAL FAULT DIAGNOSABILITY AND SECURITY/PRIVACY VERIFICATION

    Författare :Mona Noori-Hosseini; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; Temporal logic; Anonymity; Opacity; Discrete event systems.; Automation; Formal verification; Fault diagnosability; Incremental abstraction;

    Sammanfattning : Dynamical systems can be classified into two groups. One group is continuoustime systems that describe the physical system behavior, and therefore are typically modeled by differential equations. The other group is discrete event systems (DES)s that represent the sequential and logical behavior of a system. LÄS MER

  3. 22. On Formal Specification and Verification of Function Block Applications in Industrial Control Logic Development

    Författare :Oscar Ljungkrantz; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; safety logic; function block; IEC 61131; software requirements and specification; formal verification; reusable automation component RAC ; temporal logic; manufacturing automation software; programmable logic controller PLC ; model checking;

    Sammanfattning : Developing a control system for an automated manufacturing system is a challenging task. In addition to controlling and coordinating the machines and robots used in the production, the safety of the operators must be assured. LÄS MER

  4. 23. Secure System Virtualization : End-to-End Verification of Memory Isolation

    Författare :Hamed Nemati; Mads Dam; Gustavo Betarte; KTH; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Platform Security; Hypervisor; Formal Verification; Theorem Proving; HOL4; Cache attack; Security Monitor; Information Flow; Computer Science; Datalogi;

    Sammanfattning : Over the last years, security-kernels have played a promising role in reshaping the landscape of platform security on embedded devices. Security-kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms on a small TCB, which enforces isolation between components. LÄS MER

  5. 24. Graph dominators in logic synthesis and verification

    Författare :René Krenz; KTH; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; formal verification; logic synthesis; dominators; equivalence checking; decomposition; Computer science; Datavetenskap;

    Sammanfattning : This work focuses on the usage of dominators in circuit graphs in order to reduce the complexity of synthesis and verification tasks. One of the contributions of this thesis is a new algorithm for computing multiple-vertex dominators in circuit graphs. LÄS MER

  7. 25. Situation awareness in pervasive computing systems : reasoning, verification, prediction

    Författare :Andrey Boytsov; Christian Becker; Luleå tekniska universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; situation awareness; context awareness; pervasive computing; ubiquitous computing; context prediction; Pervasive Mobile Computing; Distribuerade datorsystem;

    Sammanfattning : The paradigm of pervasive computing aims to integrate the computing technologies in a graceful and transparent manner, and make computing solutions available anywhere and at any time. Different aspects of pervasive computing, like smart homes, smart offices, social networks, micromarketing applications, PDAs are becoming a part of everyday life. LÄS MER