Property-Driven Continuous Assurance of Software Designs
Safety and security critical systems and its associated software need to deliver assurance, with a high degree of confidence, that they will operate correctly and reliably when deployed. The Design for Certification (DesCert) project, part of DARPA’s Automated Rapid Certification Of Software (ARCOS) program, addresses the construction of software with the goal of increasing the rigor, composability, and efficiency of the design and verification activities, along with associated artifacts. In this presentation, we describe the DesCert approach for property-driven design and verification supporting efficient arguments, along with continuous assurance evidence generation. Efficient arguments use precise claims, validatable models (e.g., requirements, designs, architecture) and assumptions, architectural separation of concerns, reusable archetypes/tools for design and verification, and a rigorous chain of reasoning that explicitly covers all relevant aspects and details. The DesCert approach and tools have been applied to multiple case studies for integrated safety and security assurance - ArduCopter (small drone) Advanced Fail Safe System and industrial scale defense avionics platform.
In safety-critical avionics systems, specification models (e.g., architecture, requirements, env./plant/faults, safety, security) serve as the basis of all development and certification activities. The DesCert approach is centered around property-based assurance, employing formal semantics to specify properties of specification models and other development artifacts. We adopt a dual approach for certain specifications: e.g., 1) requirements are specified in our Constrained Language Enhanced Approach to Requirements (CLEAR) notation, and 2) properties that these requirements must satisfy. Model-checking of properties against the requirements model enhances confidence in its validation.
DesCert methodology tracks the development of models and software artifacts: requirements in CLEAR, architecture in RADL, source code, executables, tests etc. across each phase of the lifecycle. At each stage, specialized tools verify properties of relevant specifications/ artifacts and generate evidence in a formalized workflow ontology to show that (i) the specifications and design refinements are correct and (ii) development artifacts are accurate and consistent with requirements and exhibit requisite safety and security properties. Deployment of reusable tools and design archetypes such as sound testing theory, requirements analyzers, model checkers, ontic type checkers on code, robustly partitioned architectures, pedigreed code generators and static/dynamic code analyzers ensures repeatability of the process. This instills high confidence in assurance guarantees throughout the system’s current design refinements and subsequent enhancements.
The DesCert approach readily supports the effective and safe use of generative AI in the development process for creating requirements in the CLEAR notation, with comprehensive formal analysis and property checking to validate the requirements to ameliorate output correctness issues of generative AI. We have recently created a prototype for generative-AIassisted requirement creation — providing automation to reduce human labor. To achieve high-accuracy generation from informal requirement sources, the process incorporates role descriptions for requirement generation along with minimum system/variable/enumeration definitions and CLEAR requirement templates through prompting beforehand. Since requirements are declarative and additive, the auto-generated requirements are individually reviewable by engineers. CLEAR tools perform requirements conflicts/gaps analyses and model-checking of requirements against separately specified system properties to further eliminate hallucination and logic errors.
Devesh Bhatt, Hao Ren, Anitha Murugesan, Srivatsan Varadrajan (Honeywell Aerospace)
Shankar Natarajan, Minyoung Kim (SRI International)
Michael Ernst (University of Washington)