Sökning: "Timed Model checking"

Visar resultat 1 - 5 av 10 uppsatser innehållade orden Timed Model checking.

  1. 1. Probabilistic guarantees in model-checking with Time Petri Nets

    Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Författare :Manon Lecart; [2023]
    Nyckelord :Formal Methods; Statistical Model-Checking; Timed Automata; Timed PetriNets; Formella Metoder; Statistisk Modellkontroll; Timed Automater; Time Petri Nets;

    Sammanfattning : With the prevalence of technology and computer systems in today’s society, it is crucial to ensure that the systems we use are secure. The fields that study these issues, cybersecurity and cybersafety, use the formal verification technique of modelchecking. LÄS MER

  3. 2. Reasoning about Moving Target Defense in Attack Modeling Formalisms

    Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Författare :Gabriel Ballot; [2022]
    Nyckelord :Timed Model checking; Cyber Security; Threat Modeling; Moving Target Defense; Tidsinställd modellkontroll; Cybersäkerhet; Hotmodellering; Moving Target Defense;

    Sammanfattning : Since 2009, Moving Target Defense (MTD) has become a new paradigm of defensive mechanism that frequently changes the state of the target system to confuse the attacker. This frequent change is costly and leads to a trade-off between misleading the attacker and disrupting the quality of service. LÄS MER

  4. 3. A Modeling Language for Timed Automata

    Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Författare :Ernst Widerberg; [2021]
    Nyckelord :;

    Sammanfattning : This work details the design and implementation of a modeling language for timed automata. The primary intended use of the language TML is as an interface to controller synthesis system m2mc, which is being developed in a current KTH/Chalmers research project. LÄS MER

  5. 4. CASE STUDIES ON MODELING SECURITY IMPLICATIONS ON SAFETY

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

    Författare :Aleksandar Matović; [2019]
    Nyckelord :model-checking; security; safety-critical; rebeca; modeling security implications;

    Sammanfattning : Security is widely recognized as an important property that is tightly interdependentwith safety in safety-critical systems. The goal of this thesis is to conduct case studies on the implications that security attacks may have on the safety of these systems. LÄS MER

  7. 5. A Formal Analysis Framework For EAST-ADL Architectural Models Extended With Behavioral Specifications In Simulink

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

    Författare :Vasja Çollaku; Paolo Shestani; [2019]
    Nyckelord :UPPAAL; EAST-ADL; Simulink; MetaEdit ; Timed Automata; Brake-by-Wire; Model-Driven Development; Model Checking;

    Sammanfattning : Model-Driven Development is a development approach which is being used frequently in the automotive context in order to design models. EAST-ADL is an architectural language which models systems according to their architectural features, whereas Simulink is a tool environment which models systems according to their behavior. LÄS MER