Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study
Assurance cases are often a prerequisite for certification of critical systems. They show how a system is safe to operate, through a comprehensive argument demonstrating that each requirement has been satisfied, using suitable evidence, which often originates from formal methods. Indeed, assurance cases have the potential to improve applicability of formal methods in certification, by providing a human comprehensible presentation. Recently, we have developed Isabelle/SACM, a framework for developing assurance cases with integrated formal methods. In this paper we apply our framework to an autonomous underwater vehicle demonstrator. To achieve this we encode the SI unit system in Isabelle, to allow a data model and requirements using physical units. We present a behavioural model in the graphical RoboChart state machine language, embed the artifacts into Isabelle/SACM, and use it to demonstrate satisfaction of the requirements.