Formal Assurance Certifiable Tooling Strategy
FACTS is a NASA-sponsored project to investigate issues surrounding the qualification of formal methods tools under RTCA DO-330, as part of a larger certification of flight-critical airborne software.
The scope of the investigation includes both the general problem of achieving confidence in formal methods tools as well as the more specific problem of how to meet the qualification objectives of a particular framework, namely, RTCA’s Software Tool Qualification Considerations which we refer to by its document number DO-330. The anticipated outcome of this research is a comprehensive study that identifies qualification considerations for formal methods tools under DO-330 and its companion DO-333 (RTCA's "Formal Methods Supplement to DO-178C and DO-278A"), along with possible weakness mitigation strategies. The objectives are to 1) examine how existing state-of-the-art formal methods tools could be qualified within the DO-330 framework using a safety-driven approach; 2) address three types of formal methods tools (static analysis, model checking, and model-based development tools) and their interaction in the design, implementation, and verification stages of software development; 3) examine how the dissimilarity of these tools might be employed as a risk mitigation approach; and 4) gather strategies for making claims and producing evidence about the trustworthiness of such tools and their combinations for product safety case arguments.
We began the project with a study of the theoretical soundness issues that attend three the classes of formal methods tools: static analyzers (with Kestrel Technology’s CodeHawk abstract interpretation technology as the concrete example), model checkers (with Java PathFinder as the concrete example), and model-based development tools (with Honeywell’s HiLiTE as the concrete example). This study formed the basis for a parallel, simulated DO-330 qualification exercise for our abstract interpreter and Java PathFinder. We are currently engaged in the third major subtask of formulating risk mitigation strategies for the exposures identified in the soundness study and the two qualification case studies.
We have identified the following five classes of risk mitigation that, although not eliminating the soundness issues, help significantly address them:
- Use of dissimilar tools to evaluate a common condition. For instance, use of input/output checkers to catch common usage errors, proof checkers to verify the reasoning of a more complicated solver, etc.
- Use of redundant tools as a low-cost mechanism to identify implementation errors in the tool.
- Self-Tests and benchmarks to verify a given tool installation.
- Lifecycle enhancements to insure that a single complex tool cannot compromise the assurance case.
- Safety case argument templates to identify tool chain weaknesses that impact the rigor of an assurance case.
CertWare Argument Based Safety Assurance
CertWare ABSA developed several extensions to the Eclipse-based open source CertWare workbench. The primary motivation was to extend support earlier into the assurance lifecycle to support the development of assurance case content related to hazard analysis, hazard mitigation decisions, system state assumptions, high-level requirements and modeling, and so on. We wanted to provide alternative forms of assurance case production that better supported automated analysis such as fallacy identification, inconsistencies, or multiple conclusions. We also wanted to provide more examples to help others become familiar with the tool set and with assurance case activities. CertWare ABSA developed the following:
- Implementation of the OMG Structured Assurance Case Metamodel (SACM) editors and a companion Xtext DSL.
- Design and implementation of a new language L for writing and analyzing structured assurance case arguments using answer set programming techniques. We implemented the language editor and its results model in Xtext and provided a Prolog-based solver for Linux.
- Design and implementation of a novel technique for synthesizing fault trees from declarative models of physical systems, dubbed fault trees from physics (FTP). The implementation includes a Sirius-based graphical editor for connecting physical system components (chosen in this case a built-in library of electronics components) containing essential physical behavioral descriptions using fundamental laws. We implemented an analyzer using the CLP(R) inference engine to synthesize the combinations of possible faults and consequences which we produce as a results model.
- Implementation of models and an editing framework for gathering system specifications and hazard models using Nancy Leveson's techniques for STPA and a canonical intent specification similar to SpecTRM.
- Implementation of a state analysis metamodel and a graphical editing framework intended to promote a state elaboration procedure as part of requirements completeness assessment and hazard analysis in control system design. The main idea, template, and procedure here we adopted from NASA JPL's Mission Data System project.
- Migration of legacy content forward to Eclipse Mars.
We prepared a number of examples to illustrate various aspects of the tool collection. Among these were a reproduction in our L language of a large portion of the EUROCONTROL Reduced Vertical Separation Minimum (RVSM) public domain safety case argument, showing how the compact form of structured text was easier to read and write (and check automatically) than its graphical equivalent. We also prepared the canonical examples from the relevant OMG metamodel specifications, a number of computing system safety argument patterns provided by the UK MOD Software Systems Engineering Initiative (SSEI). We prepared L language and FTP examples derived from SAE ARP examples used for describing safety assessment processes.
During an earlier edition of this project we developed tools for writing several forms of safety case arguments. Among these were editors for the original OMG metamodels for safety case arguments and evidence, specializations of these models for notational differences for goal-structuring notation, claim-argument-evidence notation, and the EUROCONTROL variant of these. We also included an argumentation language from SRI, a theorem-writer, and a verification checklist model. To support case production planning we created a planning model meant to be integrated with case artifacts and production evolution. We prepared a collection a case project management metrics, both static and dynamic, to begin gathering empirical data to support planning estimates. The metrics were in part hooked to artifact commit histories in the change repository in order to capture accurate time stamps and artifact change indicators. We supported uncertain reasoning with a complete Xtext DSL rendering for the Hugin API, our own DSL for storing collected evidence in support of these models, and an Eclipse integration with UCLA's SamIam inference engine.
Eclipse Site GitHub