Encoding Verification Arguments to Analyze High-Level Design Certification Claims: Experiment Zero (E0)

The ASERT (Assurance Evidence for Continuously-Evolving Real-Time Systems) workgroup (ASERTW) has been investigating alternative technologies and techniques to automate certification. ASERTW’s first step was captured in a report that identifies the state of the practice and future challenges, especially the need to speed up the pace of updates to cyber-physical systems (CPSs).

The second step is what we call Experiment Zero (E0). The goal of this experiment is to test technique(s) to verify if the automation of certification arguments can help us to explain potential design/development flaws related to real-world reported problems. To conduct this experiment, we used a recent flight incident report published by the Taiwan Transportation Safety Board. Based on this report, we developed some theories of potential design shortcomings that could explain the sequence of events in this incident. Given the limited information obtained from the incident report, it is important to note that this paper does not claim that such shortcomings necessarily existed. Instead, we view this incident as a way to evaluate if and how formalizing and automating arguments can validate designs and find shortcomings if they exist.

This modeling and automatic verification experiment showed a robust process that allowed us to encode lessons learned in an executable format. This encoding can then be reused as we develop new arguments and verification procedures that can be used in new system developments. More importantly, the encoding enables the automatic integration of development activities to the production of certification evidence.