Browse Publications Technical Papers 2018-01-1948

A Methodology for Formal Requirements Validation and Automatic Test Generation and Application to Aerospace Systems 2018-01-1948

Automation of Validation and Verification (V&V) leveraging Formal Methods, and in particular Model Checking, is seeing an increasing use in the aerospace domain. In recent years, Formal Methods have been used to verify systems and software and its correctness as a way to augment traditional methods relying on simulation and testing. Recent updates to the relevant aerospace regulations (e.g. DO-178C, DO-331 and DO-333) now have explicit provisions for utilization of models and formal methods in the software development process. In a previous paper a compositional methodology for the validation of aerospace systems has been described with application to Electrical Power Generation and Distribution Systems. In this paper we present an expansion of the previous work in two directions. First, we describe the application of the methodology to the validation of aerospace proximity sensing systems (PSS) showing the effectiveness of the method to a new aerospace domain. Second, both the methodology and technology components have been expanded and applied to the PSS to enable automatic generation of verification test cases from requirements models showing a novel application of formal models and algorithms in new areas of application in the context of the aerospace domain.


Subscribers can view annotate, and download all of SAE's content. Learn More »


Attention: This item is not yet published. Pre-Order to be notified, via email, when it becomes available.