Verification and Validation of Model-Based Systems Requirements and Design Leveraging Formal Methods to Increase Development Assurance

As model-based systems engineering is proliferating throughout the aerospace industry as a method to manage the development of complex cyber-physical systems, opportunities to leverage formal methods for verification and validation purposes are significant. As a system model described in SysML can contain the level of semantics required to define strict system requirements, it is possible to create a translation tool to generate SRL (SADL (Semantic Application Design Language) Requirements Language) to leverage ASSERT™ (Analysis of Semantic Specifications and Efficient generation of requirements-based Tests) for verification and validation of the system requirements. SADL [13] is a controlled English grammar that translates directly into OWL (Web Ontology Language) [14]. As part of the validation of the SRL requirements, ASSERT™ leverages a theorem prover to look for conflict and completeness errors. For verification, ASSERT™ uses a Satisfiability Modulo Theories (SMT) solver for the generation of test cases and procedures. This paper extends the Braking System Control Unit (BSCU) portion of the Wheel Braking System (WBS) example within Appendix E of ARP4754B [2] described in [1] to demonstrate an example of capturing system requirements in Cameo using SysML, creating test cases and procedures from ASSERT™ exporting from SysML and translating to SRL/SADL, and exporting the Cameo system model data along with the test cases, test procedures, and requirements analysis data from ASSERT™ into the Rapid Assurance Curation Kit (RACK). RACK is a data curation platform which facilitates reporting on Development Assurance and safety assessments guidelines like those used for aircraft certification.