DLR-Logo -> http://www.dlr.de
DLR Portal Home | Imprint | Privacy Policy | Contact | Deutsch
Fontsize: [-] Text [+]

Formal Requirements and Model-Checking for V&V Automation of a RPAS Mission Management System

Torens, Christoph and Adolf, Florian-Michael (2015) Formal Requirements and Model-Checking for V&V Automation of a RPAS Mission Management System. In: AIAA Infotech @ Aerospace, pp. 1-13. American Institute of Aeronautics and Astronautics. AIAA Infotech @ Aerospace, 2nd Software Challenges in Aerospace Symposium, 2015-01-03 - 2015-01-09, Kissimmee, FL, USA. doi: 10.2514/6.2015-1645.

Full text not available from this repository.

Official URL: http://dx.doi.org/10.2514/6.2015-1645


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.

Item URL in elib:https://elib.dlr.de/94840/
Document Type:Conference or Workshop Item (Speech)
Title:Formal Requirements and Model-Checking for V&V Automation of a RPAS Mission Management System
AuthorsInstitution or Email of AuthorsAuthor's ORCID iDORCID Put Code
Torens, ChristophUNSPECIFIEDhttps://orcid.org/0000-0002-0651-4390UNSPECIFIED
Date:January 2015
Journal or Publication Title:AIAA Infotech @ Aerospace
Refereed publication:Yes
Open Access:No
Gold Open Access:No
In ISI Web of Science:No
Page Range:pp. 1-13
Publisher:American Institute of Aeronautics and Astronautics
Series Name:AIAA SciTech
Keywords:DO-178C, model-checking, formal requirements, software verification and validation, UAV, RPAS
Event Title:AIAA Infotech @ Aerospace, 2nd Software Challenges in Aerospace Symposium
Event Location:Kissimmee, FL, USA
Event Type:international Conference, Workshop
Event Start Date:3 January 2015
Event End Date:9 January 2015
Organizer:American Institute of Aeronautics and Astronautics
HGF - Research field:Aeronautics, Space and Transport
HGF - Program:Aeronautics
HGF - Program Themes:rotorcraft
DLR - Research area:Aeronautics
DLR - Program:L RR - Rotorcraft Research
DLR - Research theme (Project):L - The Smart Rotorcraft (old)
Location: Braunschweig
Institutes and Institutions:Institute of Flight Systems > Unmanned Aircraft
Deposited By: Torens, Christoph
Deposited On:26 Jan 2015 12:54
Last Modified:24 Apr 2024 20:00

Repository Staff Only: item control page

Help & Contact
electronic library is running on EPrints 3.3.12
Website and database design: Copyright © German Aerospace Center (DLR). All rights reserved.