Assurance Case Generation Using Model-based Engineering and Formal Verification

Assurance cases (ACs) have been a well-established means to provide compelling justifications for ensuring confidence in critical system properties. The development of ACs should follow an incremental and iterative approach, allowing them to evolve continuously and uphold their assurance validity as the system evolves. However, the generation and maintenance of ACs are labour-intensive tasks that are prone to human errors.
Model-based Engineering (MBE) has been exploited to generate model-based ACs. One of the key advantages of MBE is the traceability automatically established between system artifacts and AC models, enabling the automated creation and updates of ACs in response to system modifications. However, there are existing limitations in the current solutions, specifically in providing adequate support for generating ACs from heterogeneous notations. On the other hand, the generation of evidence remains a critical aspect of the AC process. Formal verification offers a rigorous means of providing evidence for ACs and has the potential for automation. However, there is a research gap of the insufficient automation and coordination of various formal verification techniques.
This thesis proposes a framework for automatically deriving model-based ACs from system artifacts using MBE and formal verification techniques including model checking and theorem proving. There are three main contributions in this research: a method for generating the AC structure compliant with Structured Assurance Case Metamodel from artefacts of different formats using MBE techniques; a method for refining the lower-level structure from formal syntax of robotic design models; and a method for generating AC evidence from formal semantics of robotic models by coordinating formal verification techniques including FDR and PRISM model checking, and Isabelle/HOL theorem proving. A methodology is provided to guide the joint use of these methods to produce an AC.
The framework is evaluated using four robotic systems of different natures, showing its generality across different domains. Several challenges identified in the research literature have been addressed to enhance the efficiency and effectiveness of AC generation and AC evolution within the MBE framework. Our framework provides engineers with an efficient solution for the derivation and evolution of model-based ACs. Also, the integration of automated formal verification processes significantly reduces the reliance on formal expertise, thereby promoting the practical adoption of formal verification in the AC process.