Sökning: "software model checking"

Visar resultat 26 - 30 av 57 uppsatser innehållade orden software model checking.

  1. 26. Executive Summaries in Software Model Checking

    Master-uppsats, KTH/Teoretisk datalogi, TCS

    Författare :Lasse Berglund; [2018]
    Nyckelord :program verification; software engineering; concurrent programming; model checking; software model checking;

    Sammanfattning : Model checking is a technique used to verify whether a model meets a given specification by exhaustively and automatically checking each reachable state in the model. It is a well-developed technique, but it suffers from some issues, perhaps most importantly the state space explosion problem. LÄS MER

  3. 27. A Comparative Analysis of Dynamic Software Update Methods in regard to Safety-critical Systems

    Kandidat-uppsats, Göteborgs universitet/Institutionen för data- och informationsteknik

    Författare :Max Enelund; Dennis Karlberg; Niklas le Comte; [2017-09-18]
    Nyckelord :Dynamic software update; Safety-critical; Code relinking; Reference indirection; Experiment; model checking;

    Sammanfattning : Software is an ever evolving product that is updated to extend the functionality and to reduce bugs within a system. Many systems are required to maintain a high availability to provide their services. Dynamic software update is a mechanism which allows the software to be updated during run-time. LÄS MER

  4. 28. Automatic Test Generation and Mutation Analysis using UPPAAL SMC

    Kandidat-uppsats, Mälardalens högskola/Akademin för innovation, design och teknik

    Författare :Jonatan Larsson; [2017]
    Nyckelord :UPPAAL SMC; Automatic Testing; Mutation Analysis; Test Generation; Priced Timed Automata; C#;

    Sammanfattning : Software testing is an important process for ensuring the quality of the software. As the complexity of the software increases, traditional means of manual testing becomes increasingly more complex and time consuming. In most embedded systems, designing software with as few errors as possible is often critical. LÄS MER

  5. 29. Configuring Java Pathfinder for concurrent Java programs

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

    Författare :Andrew Bwogi; Tuncay Dagdelen; [2017]
    Nyckelord :;

    Sammanfattning : Software verification is a field of computer science dedicated to guar- antee that a program runs according to a formalized specification. Of various kinds of verification techniques model checking tries all possi- ble states of a program and makes sure each state satisfies a set of for- malized properties. LÄS MER

  7. 30. Lightweight Software Isolation via Flow-Sensitive Capabilities in Scala

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

    Författare :Erik Reimers; [2017]
    Nyckelord :Scala; LaCasa; flow-sensitive; aliasing;

    Sammanfattning : Aliasing is a potential source of problems in software development and can, for example,lead to data races in concurrent programs. More recent programming languages includealiasing control in order to catch more errors at compile time. However, this does notexist for most widely-used languages.LaCasa introduces aliasing control to Scala. LÄS MER