Sökning: "formell verifiering"

Visar resultat 1 - 5 av 7 avhandlingar innehållade orden formell verifiering.

  1. 1. Formal Verification of Peripheral Memory Isolation

    Författare :Jonas Haglund; Roberto Guanciale; Mads Dam; Gligor Virgil; KTH; []
    Nyckelord :TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; formal verification; interactive theorem proving; direct memory access; memory isolation; input output; formell verifiering; interaktiv datorassisterad beviskonstruktion; direkt minnesåtkomst; minnesisolering; indata utdata; Datalogi; Computer Science;

    Sammanfattning : In many contexts, computers run both critical and untrusted software,necessitating the need for isolating critical software from untrusted software.These computers contain CPUs, memory and peripherals. LÄS MER

  3. 2. Proving Safety and Security of Binary Programs

    Författare :Andreas Lindner; Roberto Guanciale; Mads Dam; Tamara Rezk; KTH; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Binary Code; Binary Analysis; Formal Verification; Model-Based Testing; Theorem Proving; HOL4; Intermediate Language; Instruction Set Architectures; ISA; Observational Models; Symbolic Execution; Weakest-Precondition; Execution Time Analysis; binärkod; binärkodsanalys; formell verifiering; modellbaserad testning; satsbevisning; HOL4; mellankod; instruktionsuppsättningar; ISA; observationsmodeller; symbolisk exekvering; minst restriktiva villkoret; analys av övre tidsgräns; Datalogi; Computer Science;

    Sammanfattning : With the increasing ubiquity of computing devices, their correct and secure operation is of growing importance. In particular, critical components that provide core functionalities or process sensitive data have to operate as intended. LÄS MER

  4. 3. Towards a Trustworthy Stack: Formal Verification of Low-Level Hardware and Software

    Författare :Ning Dong; Roberto Guanciale; Mads Dam; Magnus Myreen; KTH; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Formal Verification; Information Flow; Refinement; Interactive Theorem Prover; HOL4; Serial Interface; Pipelined Processor; Microarchitecture; Out-of-order Execution; Formell Verifiering; Informationsflöde; Förfining; Interaktiva Bevisprogrammet; HOL4; Seriellt Gränssnitt; Pipelined Processor; Mikroarkitektur; Omordnad Exekvering; Datalogi; Computer Science;

    Sammanfattning : Computer systems, consisting of hardware and software, have gained significant importance in the digitalised world. These computer systems rely on critical components to provide core functionalities and handle sensitive data. LÄS MER

  5. 4. A Formal Approach to Embedded High-Integrity Real-Time Systems

    Författare :Gustaf Naeser; Lars Asplund; Juan de la Puente; Mälardalens högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Computer science; Datavetenskap; Datavetenskap;

    Sammanfattning : Den här avhandlingen handlar inte om obskyra teoretiska datavetenskapliga hemligheter, den handlar om hur datorsystem kan göras säkrare. Ur ett annat perspektiv kan den sägas försöka sig på att göra svåra metoder, som formella sådana, lättare att använda så att fler programmerare och systemdesigners kan dra nytta av dem. LÄS MER

  7. 5. Enabling Tool Support for Formal Analysis of ECA Rules

    Författare :AnnMarie Ericsson; Sten F. Andler; José Júlio Alferes; Linköpings universitet; []
    Nyckelord :ECA rules; Timed automata; Formal veri¯cation; TECHNOLOGY; TEKNIKVETENSKAP; Teknik;

    Sammanfattning : Rule-based systems implemented as event-condition-action (ECA) rules utilize a powerful and flexible paradigm when it comes to specifying systems that need to react to complex situation in their environment. Rules can be specified to react to combinations of events occurring at any time in any order. LÄS MER