Formal Modelling of the Impact of Cyberattacks on Safety of Networked Control Systems

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.