Generation and Verification of Executable Assurance Case by Model-based Engineering

TY - GEN

T1 - Generation and Verification of Executable Assurance Case by Model-based Engineering

AU - Yan, Fang

N1 - This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details

PY - 2021/8/27

Y1 - 2021/8/27

N2 - Assurance Cases (ACs) are used for justifying system confidence in important properties including safety, reliability, etc. Their manual generation is time-consuming and prone to errors. Also, AC update calls for more labour. However, there is not an automatic solution to guide the whole engineering process of AC generation and verification process. An executable AC is machine readable and checkable, and brings the benefit of efficiency and confidence of AC evolution. Thus, in this PhD, the Model-based Engineering (MBE) techniques are exploited for an automatic process for executable ACs. The first aim is to generate AC models automatically from system artefacts. Currently available approaches are usually constrained to specific modelling environments, or address only system model artefacts, or do not cover informal and unstructured artefacts. The second aim is to automate the evidence generation using formal verification. FM provides a rigorously mathematical proof. But current solutions to create formal assertions are manual and expertise-requiring. The paper discusses on the technical problem, and the proposed approach.

AB - Assurance Cases (ACs) are used for justifying system confidence in important properties including safety, reliability, etc. Their manual generation is time-consuming and prone to errors. Also, AC update calls for more labour. However, there is not an automatic solution to guide the whole engineering process of AC generation and verification process. An executable AC is machine readable and checkable, and brings the benefit of efficiency and confidence of AC evolution. Thus, in this PhD, the Model-based Engineering (MBE) techniques are exploited for an automatic process for executable ACs. The first aim is to generate AC models automatically from system artefacts. Currently available approaches are usually constrained to specific modelling environments, or address only system model artefacts, or do not cover informal and unstructured artefacts. The second aim is to automate the evidence generation using formal verification. FM provides a rigorously mathematical proof. But current solutions to create formal assertions are manual and expertise-requiring. The paper discusses on the technical problem, and the proposed approach.

UR - https://github.com/laila-fangyan/SACM-AC-generation-use-case.git

M3 - Conference contribution

BT - 2021 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)

ER -