A Composite Safety Assurance Method for Developing System Architecture Using Model Checking

1. Introduction

As system assurance is the discipline that identifies and mitigates or removes exploitable vulnerabilities, it is increasingly important for both commercial and governmental activities. In the process of system development, dependability analysis for system components and functions is generally considered to be indispensable (Sommerville, 2015). As for system assurance, conventionally, the certifier determines the safety of a system through checklist items, there were few explicit discussions about why the system was safe if the checklist items were met. Where the safety of a system needs to be explained to a third party or stakeholders, the checklist items may not be sufficient to prove that the system is truly safe. When it is necessary to explain the safety of a system to a third party, it may be necessary not only to present the checklist items, but also to explain why those procedures and tests assure safety. In this case, developing assurance cases is a common measure. The assurance case (International Organization for Standardization 15026-1:2019, 2019) is a document for discussing the safety of a system based on the test results and verification results as evidence.

An assurance case is a structured argument, supported by evidence, used to demonstrate that a system exhibits some complex properties such as safety, security or reliability in a given environment. Assurance cases focused on safety are usually called “safety cases”. System architecture provides visualization of system elements and relationships, assurance case provides evidence of system dependability. Although the development of assurance case is often based on system architecture or system model, assurance cases have been developed independent of system architectures, the relationships between system architecture and assurance cases are often ambiguous, it would be difficult for third parties to grasp which components of the system are specifically addressed by the safety issues in the assurance case. Therefore, it is worth considering a new modeling method to combine system elements and assurance cases to make the system assurance more intuitive and effective. Besides, Assurance cases are often applied to safety-critical systems, which often have complex interactions or state transitions. However, it is difficult to show the dependability of the complex interactions by using only assurance cases because assurance case arguments are predominantly inductive rather than deductive.

Consequently, in order to make it easier to explain the dependability of the system to third parties and make the system assurance more intuitive and effective, this study tries to propose a composite safety assurance approach based on the 4-steps as follows.