Formal Modelling of the Impact of Cyberattacks on Safety of Networked Control Systems
Time: Thu 2025-05-08 14.00
Location: F3 (Flodis), Lindstedtsvägen 26 & 28, Campus
Language: English
Subject area: Computer Science
Doctoral student: Ehsan Poorhadi , Teoretisk datalogi, TCS
Opponent: Professor Yamine Aït Ameur, IRIT/INPT-ENSEEIHT, University of Tolouse, France
Supervisor: Professor Elena Troubitsyna, Teoretisk datalogi, TCS
QC 20250417
Abstract
Modern control systems provide services that are indispensable for society, e.g., transportation, energy production, healthcare etc. Hence, it is important to guarantee safe and reliable functioning of such systems. However, they are increasingly relying on networking technologies, which makes them susceptible to cyberattacks that could potentially jeopardise their safety. Moreover, such systems typically have a complex distributed architecture and dynamic behaviour. Hence, it is hard to ensure correctness and safety of their design. Formal methods are used to tackle system complexity and guarantee correctness of the design via abstract mathematical modelling and rigorous verification. Various formal modelling techniques have been successfully used in the design of safety-critical systems in different domains. However, they primarily focused on modelling and verification of system safety. Since modern safety-critical systems are increasingly becoming the subject of cyberattacks, formal modelling techniques should be extended to address the emerging problem of safety-security interactions. In this thesis, we propose a rigorous approach to modelling the impact of cyberattacks on safety of networked control systems. Our approach integrates graphical modelling in Systems Modelling Language – SysML and formal specification and verification in the Event-B framework. Graphical models provide support in visualising system architecture and interactions between the components as well as facilitate the analysis of safety and security interactions by the interdisciplinary teams. Modelling and proof- based verification in Event-B allows us to formally identify the cyberattacks that jeopardise system safety. To bridge the gap between the graphical and formal modelling, we developed software automatically translating graphical system models into formal specifications in Event-B. We believe that this thesis makes both theoretical and practical contributions towards an integration of safety and security engineering, which is necessary for the development of modern trustworthy networked control systems.