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.

Moderna reglersystem tillhandahåller tjänster som är oumbärliga för samhället, t.ex. transport, energiproduktion, hälso- och sjukvård etc. Därför är det viktigt att garantera att sådana system fungerar säkert och tillförlitligt. De använder dock i allt högre grad nätverksteknik, vilket gör dem mottagliga för cyberattacker som potentiellt kan äventyra deras säkerhet. Dessutom har sådana system vanligtvis komplex distribuerad arkitektur och dynamiskt beteende. Därför är det svårt att säkerställa att deras design är korrekt och säker. Formella metoder används för att hantera systemkomplexitet och garantera att designen är korrekt via abstrakt matematisk modellering och rigorös verifiering. Olika formella modelleringstekniker har framgångsrikt använts vid design av trygghet-kritiska system inom olika domäner. För närvarande kräver användningen av nätverksteknik en utvidgning av denna teknik för att ta itu med det framväxande problemet med interaktion mellan trygghet och säkerhet. I den här avhandlingen föreslår vi ett rigoröst tillvägagångssätt för modellering av effekterna av cyberattacker på trygghet i nätverksanslutna styrsystem. Vårt tillvägagångssätt integrerar grafisk modellering i Systems Modelling Language – SysML och formell specifikation och verifiering i Event- B-ramverket. Grafiska modeller ger stöd för att visualisera systemarkitektur och interaktioner mellan komponenterna samt underlättar analysen av säkerhets- och trygghetsinteraktioner av de tvärvetenskapliga teamen. Modellering och bevisbaserad verifiering i Event-B gör det möjligt för oss att formellt identifiera de cyberattacker som äventyrar systems trygghet. För att överbrygga klyftan mellan den grafiska och formella modelleringen utvecklade vi en programvara som automatiskt översätter grafiska systemmodeller till formella specifikationer i Event-B. Vi tror att denna avhandling ger både teoretiska och praktiska bidrag till en integration av säkerhets- och trygghetsteknik, vilket är nödvändigt för utvecklingen av moderna pålitliga nätverksbaserade reglersystem.