Abstract State Machines and System Theoretic Process Analysis for Safety-Critical Systems

Al-Shareefi, F ORCID: 0000-0002-5537-6086, Lisitsa, A and Dixon, C ORCID: 0000-0002-4610-9533 (2017) Abstract State Machines and System Theoretic Process Analysis for Safety-Critical Systems. In: 20th Brazilian Symposium on Formal Methods, Recife, Brazil.

Text Abstract State Machines and System Theoretic Process Analysis for Safety-Critical Systems.pdf - Author Accepted Manuscript Download (415kB)

Abstract

The Abstract State Machine (ASM) method is a formal specification and modeling technique that allows us to specify computational systems at the required abstraction level and facilitates formal analysis and verification. System Theoretic Process Analysis (STPA) is a semi-formal hazard analysis method that aims to identify safety requirements emerging from the analysis of potential interactions among components and inadequate control in the system’s design. In this paper, we combine these two techniques to develop a methodology capturing both the formal representation of ASM with the ability to generate safety properties from the STPA hazard analysis. This has the advantages of verifying the STPA requirements in a formal way, and giving insights for the improvement of the ASM specification, depending on these requirements. We illustrate our methodology by applying it to an insulin pump control system case study, showing what safety issues it highlights.

Item Type:	Conference or Workshop Item (Unspecified)
Uncontrolled Keywords:	Abstract State Machines, System Theoretic Process, Analysis, Temporal logic, Validation, Verification
Depositing User:	Symplectic Admin
Date Deposited:	19 Sep 2017 08:15
Last Modified:	19 Jan 2023 06:54
DOI:	10.1007/978-3-319-70848-5_3
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3009511