Using Formal Requirements and Model-Checking for Verification and Validation of an Unmanned Rotorcraft

Abstract

The aerospace domain is a safety-critical domain. Therefore software has to be of high quality. Software development and testing in safety-critical domains is regulated by standards, such as DO-178B and DO-178C for the aerospace domain. However, the test approach in these standards is stochastic in nature, which means that errors in the code are tried to be identified by a large set of test cases. The trust in such software products and the overall quality is achieved by traceability to requirements and strict coverage criteria as well as general conformance to processes and rigorous documentation, but any absence of errors can usually not be proved. On the other hand, the use of formal methods for software, which is now standardized by the introduction of the Supplement DO-333, promises a true validation of certain safety-critical properties. This paper shows how formal requirements and model-checking were introduced to our test strategy for an automated planning and guidance software module. The requirements for an existing software artifact were elicited and then formalized into Linear Temporal Logic and Computation Tree Logic, which are two derivatives of temporal logic. A formal model for the software was developed and NuSMV was used as a model-checking tool to analyze the requirements in regards to the model. Furthermore, the corresponding certifcation considerations for this formal method are discussed according to the relevant standards.