Combining System-Theoretic Process Analysis with formal verification for safety demonstration of an all-electric actuation system

Abstract

Komplekse sikkerhetssystemer blir stadig mer synlige i industriløsninger, noe som nødvendiggjør mer avanserte metoder for sikkerhetsanalyse. Det er særlig relevant ved utforskningen av nye tilnærminger for sikkerhetsventiler i undervannsbrønner. Overgangen fra tradisjonell elektro-hydraulisk ventilaktuering til helelektrisk ventilaktuering introduserer en ny dimensjon av programvare i sikkerhetssystemer, som krever høy pålitelighet. For å oppnå dette, gjennomføres en System-Theoretic Process Analysis (STPA), som er kjent for å være egnet for programvaretunge systemer, for å demonstrere sikkerheten til det helelektriske systemet. STPA har imidlertid sine begrensinger, som manglende evne til å takle inkonsistente krav og at det tilbyr utilstrekkelig validering av programvaren.

For å takle disse utfordringene undersøker denne masteroppgaven en ny tilnærming til STPA ved å introdusere formelle verifiseringsmetoder for å styrke sikkerhetsgarantien til det helelektriske ventilsystemet. For å oppnå dette ble en ny metode utviklet ved å manipulere den eksisterende utvidelsen SE-STPA for å lage SE-STPA-mod-metoden, ved å endre på rekkefølgen og fjerne cybersikkerhetsaspektet med SE-STPA. Å integrere formell verifisering i sikkerhetsanalysen bidrar til økt tillit til programvaren. Dette er på grunn av matematiske bevis og matematiske definisjoner av systemets sikkerhetsegenskaper. Bevisene genereres basert på modellen i det egnede formelle språket for å bevise konsistens og korrekthet i modellen, ved å sikre at variabler er tydelig definert, at begrensninger til systemet ikke brytes og at systemets dynamikk er gjennomførbar. Formelle metoder tilrettelegger for en systematisk gjennomgang og utforskning av systemoppførselen ved å modellere krav formelt, som fører til en ny måte å identifisere krav på, og redusere potensielle programvarefeil tidlig i utviklingen.

Denne masteroppgaven har bidratt til å forsøke å redusere risiko i sikkerhetskritiske systemer ved å utvikle en ny metodikk, SE-STPA-mod. Bruken av denne metoden bidrar til redusere tvetydigheter gjennom konstruksjon av en formell modell, og gjennomføring av en omfattende STPA. Ved å sikre at modellen kontinuerlig verifiseres matematisk, kan systemets logikk garanteres å være korrekt og pålitelig fra start. Dette har spesifikt blitt brukt på det helelektriske ventilsystemet, og har resultert i en systematisk verifisert modell. Tilnærmingen legger grunnlag for nye strategier for risikoredusering i sikkerhetskritiske systemer. Selv om sikkerhetsanalysen som er presentert er et betydelig skritt fremover, er den ikke endelig. Komplekse systemer er dynamiske og stadig i utvikling, noe som nødvendiggjør kontinuerlig forbedring av analysemetodikker. Fremtidig forskning bør utforske flere metoder, teknikker og verktøy for å fremme sikkerhetsdemonstrasjon, og sikre tryggere og mer pålitelig systemdrift og programvare.

Reliable and complex systems are becoming increasingly integral to industry solutions, necessitating more advanced safety analysis methodologies. This is particularly relevant in the exploration of novel approaches for safety valve actuation in subsea wells. The shift from traditional electro-hydraulic actuation to all-electric valve actuation introduces a new dimension of software-intensive safety systems, which require robust safety assurance mechanisms. To do so, System-Theoretic Process Analysis (STPA), known for being a suitable method for software-intensive systems, is conducted to create suitable constraints and demonstrate safety of the all-electric system. However, STPA has its limitations, such as the inability to tackle potential inconsistencies in requirements and insufficient validation of software systems.

To address these challenges, this thesis investigates an integrated approach to safety analysis by combining STPA with formal verification to strengthen the safety assurance of the all-electric actuation system. This is achieved by customizing the Security-Enhanced STPA (SE-STPA) to consider safety instead of security, resulting in a new methodology, SE-STPA-mod. SE-STPA-mod combines STPA with formal verification to validate system behavior and reduce ambiguities in STPA.

Incorporating formal verification in the safety analysis provides increased confidence in the software due to mathematical proofs of the system's safety properties. The proofs are generated by the suitable formal language to prove consistency and correctness of the model, by ensuring variables are well-defined, that constraints are not violated through the modelling and that the dynamics in the system are feasible. Additionally, formal methods allow for systematic exploration of system behavior by formally modeling every requirement. Having to model the system formally introduces a new way of identifying requirements, reducing potential software errors early in the development.

This thesis contributes to reducing risks in safety-critical systems by delineating a novel methodology - SE-STPA-mod. It elaborates on its application in constructing a formal model, as well as conducting an STPA, that effectively minimizes ambiguities. By ensuring continuous adherence to each constraint throughout the modelling process by the help of mathematical proof, a correct-by-construction software logic is created. Specifically, this approach has been employed for the all-electric actuation system, yielding a systematically verified model that underscores safety and reliability. While the safety analysis presented is a substantial step forward, it is not definitive. Complex systems are dynamic and constantly evolving, necessitating continuous improvement in safety analysis methodologies. Future research should explore additional methods, techniques, and tools to advance the safety analysis process, ensuring safer and more dependable system operation.