Doktorandské kolokvium KAI - Ismaila Jesse Mazadu (15.6.2026)
v pondelok 15.6.2026 o 13:10 hod. v miestnosti I 9
Prednášajúci: Ismaila Jesse Mazadu
Názov: RUNTIME VERIFICATION FOR DETECTING CYBER-PHYSICAL ATTACKS
Termín: 15.6.2026, 13:10 hod., I 9
Abstrakt:
Runtime Verification (RV) is a lightweight yet rigorous technique that serves as a practical complement to traditional exhaustive formal verification methods, such as model checking, testing and theorem proving, especially when dealing with complex or large-scale systems. Rather than depending on a detailed, fine-grained model of the system (for instance, a low-level re-implementation down to individual instructions), RV focuses on observing and analyzing the actual execution traces produced by the running system. These traces are then checked against a formal specification that defines the expected (or forbidden) behavior. One key strength of this approach is that RV delivers accurate insights into the system’s real runtime behavior, by-passing the challenges and potential inaccuracies associated with manually creating comprehensive models in a dedicated modeling language. Runtime verification is the basis for concepts dealing with observed faults and cyberattacks on a system. Verification comprises all techniques suitable for showing that a system satisfies its specification. Runtime Verification enables reacting to faults before they become failures at the time of execution. This enables applications of runtime verification techniques that other verification techniques cannot support. Runtime verification can now be seen as the discipline of computer science that deals with the study, development, and application of verification techniques that allow checking whether a run of a system under scrutiny satisfies or violates a given correctness property. The main purpose of this study is to review previous literature on Runtime Verification and to develop a robust Runtime Verification framework that will detect cyber-physical attacks, prevent them, and ensure the safety and liveliness of a system in operation. The study proposes Runtime Verification for UAVs using a Dynamic CEE-TeSSLa-based Framework, to enforce security, safety, and liveliness of the UAVs