Model-based Generation of Hazard-driven Arguments and Formal Verification Evidence for Assurance Cases

Abstract

Assurance cases (ACs) are an established practice for arguing confidence in critical system properties such as safety and security in high-risk industries.ACs use system artifacts to argue the aforementioned properties.Due to the iterative nature of system development, we need to update ACs to maintain assurance validity as a system evolves.For example, a changed design or an added hazard would result in re-evaluation of claims or a new claim to be verified.Thus, the generation and maintenance of ACs is a labour-intensive process.With the growing application of Model-based Engineering (MBE) in system development, it is beneficial to generate ACs from design models because this captures traceability, and enables automatic AC creation and update driven by model modification.Accordingly, the contribution of this paper is an automatic approach to AC generation and assembly from both unstructured design artifacts and UML-like design models within Eclipse.This approach also supports AC evidence generation by formal verification facilitated by automatically generated assertions.The realization of AC assembly and verification is supported by model query and model transformation.We apply our approach to an autonomous underwater robot with the RoboChart robotics modelling language.