elib
DLR-Header
DLR-Logo -> http://www.dlr.de
DLR Portal Home | Impressum | Kontakt | English
Schriftgröße: [-] Text [+]

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

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

Dieses Archiv kann nicht den gesamten Text zur Verfügung stellen.

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

Kurzfassung

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.

Dokumentart:Konferenzbeitrag (Vortrag)
Titel:Formal Requirements and Model-Checking for V&V Automation of a RPAS Mission Management System
Autoren:
AutorenInstitution oder E-Mail-AdresseAutoren-ORCID
Torens, Christophchristoph.torens@dlr.deNICHT SPEZIFIZIERT
Adolf, Florian-Michaelflorian.adolf@dlr.deNICHT SPEZIFIZIERT
Datum:Januar 2015
Erschienen in:AIAA Infotech @ Aerospace
Referierte Publikation:Ja
In Open Access:Nein
In SCOPUS:Nein
In ISI Web of Science:Nein
DOI :10.2514/6.2015-1645
Seitenbereich:Seiten 1-13
Verlag:American Institute of Aeronautics and Astronautics
Name der Reihe:AIAA SciTech
Status:veröffentlicht
Stichwörter:DO-178C, model-checking, formal requirements, software verification and validation, UAV, RPAS
Veranstaltungstitel:AIAA Infotech @ Aerospace, 2nd Software Challenges in Aerospace Symposium
Veranstaltungsort:Kissimmee, FL, USA
Veranstaltungsart:internationale Konferenz, Workshop
Veranstaltungsdatum:03.-09. Jan. 2015
Veranstalter :American Institute of Aeronautics and Astronautics
HGF - Forschungsbereich:Luftfahrt, Raumfahrt und Verkehr
HGF - Programm:Luftfahrt
HGF - Programmthema:Hubschrauber
DLR - Schwerpunkt:Luftfahrt
DLR - Forschungsgebiet:L RR - Rotorcraft Research
DLR - Teilgebiet (Projekt, Vorhaben):L - Der intelligente Drehflügler
Standort: Braunschweig
Institute & Einrichtungen:Institut für Flugsystemtechnik > Unbemannte Luftfahrzeuge
Hinterlegt von: Torens, Christoph
Hinterlegt am:26 Jan 2015 12:54
Letzte Änderung:15 Dez 2016 15:38

Nur für Mitarbeiter des Archivs: Kontrollseite des Eintrags

Blättern
Suchen
Hilfe & Kontakt
Informationen
electronic library verwendet EPrints 3.3.12
Copyright © 2008-2013 Deutsches Zentrum für Luft- und Raumfahrt (DLR). Alle Rechte vorbehalten.