ASCA Inc

Formal Framework and Models for Validation and Verification of Software- Intensive Aerospace Systems
January 13, 2017

Formal Framework and Models for Validation and Verification of Software- Intensive Aerospace Systems

Model-based control systems (MBCSs) and adaptive control systems (ACSs) represent an emerging class of software-intensive space and aeronautical control applications that bring tangible benefits to design processes and developments, but also challenges to traditional validation and verification (V&V) methods. This paper presents the results produced in the first two years of a three-year NASA project seeking the development of a comprehensive framework for the V&V of MBCSs and ACSs. The framework under development represents a comprehensive V&V methodology that utilizes Dynamic Flowgraph Methodology (DFM) and Markov-CCMT (Cell to Cell Mapping Technique) logic-dynamic model constructs, and associated time-dependent, deductive-inductive multi-valued logic analysis processes. This V&V framework produces formal evidence supporting the generation and documentation of an assurance case for a model-based control system, for the ultimate objective of demonstrating its compliance.

S. Guarro, M. Yau, et al, “Formal Framework and Models for Validation and Verification of Software- Intensive Aerospace Systems,” Proceedings of the 2017 AIAA SciTech Forum, Grapevine, Texas, January 9-13, 2017

ASCA Inc.

Quick Navigation