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

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publication2021 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)
Publication statusAccepted/In press - 27 Aug 2021

Bibliographical note

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

Cite this