Approaches for software verification of an emergency recovery system for Micro Air Vehicles

Martin Becker; Markus Neumair; Alexander Söhn; Samarjit Chakraborty

doi:10.1007/978-3-319-24249-1_32

Approaches for software verification of an emergency recovery system for Micro Air Vehicles

Martin Becker, Markus Neumair, Alexander Söhn, Samarjit Chakraborty

Chair of Real-Time Computer Systems

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

2 Scopus citations

Abstract

This paper describes the development and verification of a competitive parachute system for Micro Air Vehicles, in particular focusing on verification of the embedded software. We first introduce the overall solution including a system level failure analysis, and then show how we minimized the influence of faulty software. This paper demonstrates that with careful abstraction and little overapproximation, the entire code running on a microprocessor can be verified using bounded model checking, and that this is a useful approach for resource-constrained embedded systems. The resulting Emergency Recovery System is to our best knowledge the first of its kind that passed formal verification, and furthermore is superior to all other existing solutions (including commercially available ones) from an operational point of view.

Original language	English
Title of host publication	Computer Safety, Reliability, and Security - AFECOMP 2015 Workshops ASSURE, DECSoS, ISSE, ReSA4CI, and SASSUR, Proceedings
Editors	Coen van Gulijk, Floor Koornneef
Publisher	Springer Verlag
Pages	369-385
Number of pages	17
ISBN (Print)	9783319242484
DOIs	https://doi.org/10.1007/978-3-319-24249-1_32
State	Published - 2015
Event	International Conference on Computer Safety, Reliability, and Securitym, SAFECOMP 2015 and held 3rd International Workshop on Assurance Cases for Software-Intensive Systems ASSURE 2015, Workshop on Dependable Embedded and Cyber-Physical Systems and Systems-of-Systems, DECSoS 2015, 2nd International Workshop on the Integration of Safety and Security Engineering, ISSE 2015, Workshop on Reliability and Security Aspects for Critical Infrastructure Protection, ReSA4CI 2015, and 4th InternationalWorkshop on NextGeneration of System Assurance Approaches for Safety-Critical Systems SASSUR, 2015 - Delft, Netherlands Duration: 22 Sep 2015 → 22 Sep 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9338
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Computer Safety, Reliability, and Securitym, SAFECOMP 2015 and held 3rd International Workshop on Assurance Cases for Software-Intensive Systems ASSURE 2015, Workshop on Dependable Embedded and Cyber-Physical Systems and Systems-of-Systems, DECSoS 2015, 2nd International Workshop on the Integration of Safety and Security Engineering, ISSE 2015, Workshop on Reliability and Security Aspects for Critical Infrastructure Protection, ReSA4CI 2015, and 4th InternationalWorkshop on NextGeneration of System Assurance Approaches for Safety-Critical Systems SASSUR, 2015
Country/Territory	Netherlands
City	Delft
Period	22/09/15 → 22/09/15

Keywords

Formal analysis
Multicopter
Parachute
Remotely-piloted aircraft systems
Safety
Software verification

Access to Document

10.1007/978-3-319-24249-1_32

Cite this

Becker, M., Neumair, M., Söhn, A., & Chakraborty, S. (2015). Approaches for software verification of an emergency recovery system for Micro Air Vehicles. In C. van Gulijk, & F. Koornneef (Eds.), Computer Safety, Reliability, and Security - AFECOMP 2015 Workshops ASSURE, DECSoS, ISSE, ReSA4CI, and SASSUR, Proceedings (pp. 369-385). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9338). Springer Verlag. https://doi.org/10.1007/978-3-319-24249-1_32

Becker, Martin ; Neumair, Markus ; Söhn, Alexander et al. / Approaches for software verification of an emergency recovery system for Micro Air Vehicles. Computer Safety, Reliability, and Security - AFECOMP 2015 Workshops ASSURE, DECSoS, ISSE, ReSA4CI, and SASSUR, Proceedings. editor / Coen van Gulijk ; Floor Koornneef. Springer Verlag, 2015. pp. 369-385 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4735fb86157143f6bee8aa25f0ded6d1,

title = "Approaches for software verification of an emergency recovery system for Micro Air Vehicles",

abstract = "This paper describes the development and verification of a competitive parachute system for Micro Air Vehicles, in particular focusing on verification of the embedded software. We first introduce the overall solution including a system level failure analysis, and then show how we minimized the influence of faulty software. This paper demonstrates that with careful abstraction and little overapproximation, the entire code running on a microprocessor can be verified using bounded model checking, and that this is a useful approach for resource-constrained embedded systems. The resulting Emergency Recovery System is to our best knowledge the first of its kind that passed formal verification, and furthermore is superior to all other existing solutions (including commercially available ones) from an operational point of view.",

keywords = "Formal analysis, Multicopter, Parachute, Remotely-piloted aircraft systems, Safety, Software verification",

author = "Martin Becker and Markus Neumair and Alexander S{\"o}hn and Samarjit Chakraborty",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; International Conference on Computer Safety, Reliability, and Securitym, SAFECOMP 2015 and held 3rd International Workshop on Assurance Cases for Software-Intensive Systems ASSURE 2015, Workshop on Dependable Embedded and Cyber-Physical Systems and Systems-of-Systems, DECSoS 2015, 2nd International Workshop on the Integration of Safety and Security Engineering, ISSE 2015, Workshop on Reliability and Security Aspects for Critical Infrastructure Protection, ReSA4CI 2015, and 4th InternationalWorkshop on NextGeneration of System Assurance Approaches for Safety-Critical Systems SASSUR, 2015 ; Conference date: 22-09-2015 Through 22-09-2015",

year = "2015",

doi = "10.1007/978-3-319-24249-1_32",

language = "English",

isbn = "9783319242484",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "369--385",

editor = "{van Gulijk}, Coen and Floor Koornneef",

booktitle = "Computer Safety, Reliability, and Security - AFECOMP 2015 Workshops ASSURE, DECSoS, ISSE, ReSA4CI, and SASSUR, Proceedings",

}

Becker, M, Neumair, M, Söhn, A & Chakraborty, S 2015, Approaches for software verification of an emergency recovery system for Micro Air Vehicles. in C van Gulijk & F Koornneef (eds), Computer Safety, Reliability, and Security - AFECOMP 2015 Workshops ASSURE, DECSoS, ISSE, ReSA4CI, and SASSUR, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9338, Springer Verlag, pp. 369-385, International Conference on Computer Safety, Reliability, and Securitym, SAFECOMP 2015 and held 3rd International Workshop on Assurance Cases for Software-Intensive Systems ASSURE 2015, Workshop on Dependable Embedded and Cyber-Physical Systems and Systems-of-Systems, DECSoS 2015, 2nd International Workshop on the Integration of Safety and Security Engineering, ISSE 2015, Workshop on Reliability and Security Aspects for Critical Infrastructure Protection, ReSA4CI 2015, and 4th InternationalWorkshop on NextGeneration of System Assurance Approaches for Safety-Critical Systems SASSUR, 2015, Delft, Netherlands, 22/09/15. https://doi.org/10.1007/978-3-319-24249-1_32

Approaches for software verification of an emergency recovery system for Micro Air Vehicles. / Becker, Martin; Neumair, Markus; Söhn, Alexander et al.
Computer Safety, Reliability, and Security - AFECOMP 2015 Workshops ASSURE, DECSoS, ISSE, ReSA4CI, and SASSUR, Proceedings. ed. / Coen van Gulijk; Floor Koornneef. Springer Verlag, 2015. p. 369-385 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9338).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Approaches for software verification of an emergency recovery system for Micro Air Vehicles

AU - Becker, Martin

AU - Neumair, Markus

AU - Söhn, Alexander

AU - Chakraborty, Samarjit

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2015.

PY - 2015

Y1 - 2015

N2 - This paper describes the development and verification of a competitive parachute system for Micro Air Vehicles, in particular focusing on verification of the embedded software. We first introduce the overall solution including a system level failure analysis, and then show how we minimized the influence of faulty software. This paper demonstrates that with careful abstraction and little overapproximation, the entire code running on a microprocessor can be verified using bounded model checking, and that this is a useful approach for resource-constrained embedded systems. The resulting Emergency Recovery System is to our best knowledge the first of its kind that passed formal verification, and furthermore is superior to all other existing solutions (including commercially available ones) from an operational point of view.

AB - This paper describes the development and verification of a competitive parachute system for Micro Air Vehicles, in particular focusing on verification of the embedded software. We first introduce the overall solution including a system level failure analysis, and then show how we minimized the influence of faulty software. This paper demonstrates that with careful abstraction and little overapproximation, the entire code running on a microprocessor can be verified using bounded model checking, and that this is a useful approach for resource-constrained embedded systems. The resulting Emergency Recovery System is to our best knowledge the first of its kind that passed formal verification, and furthermore is superior to all other existing solutions (including commercially available ones) from an operational point of view.

KW - Formal analysis

KW - Multicopter

KW - Parachute

KW - Remotely-piloted aircraft systems

KW - Safety

KW - Software verification

UR - http://www.scopus.com/inward/record.url?scp=84969850401&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-24249-1_32

DO - 10.1007/978-3-319-24249-1_32

M3 - Conference contribution

AN - SCOPUS:84969850401

SN - 9783319242484

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 369

EP - 385

BT - Computer Safety, Reliability, and Security - AFECOMP 2015 Workshops ASSURE, DECSoS, ISSE, ReSA4CI, and SASSUR, Proceedings

A2 - van Gulijk, Coen

A2 - Koornneef, Floor

PB - Springer Verlag

T2 - International Conference on Computer Safety, Reliability, and Securitym, SAFECOMP 2015 and held 3rd International Workshop on Assurance Cases for Software-Intensive Systems ASSURE 2015, Workshop on Dependable Embedded and Cyber-Physical Systems and Systems-of-Systems, DECSoS 2015, 2nd International Workshop on the Integration of Safety and Security Engineering, ISSE 2015, Workshop on Reliability and Security Aspects for Critical Infrastructure Protection, ReSA4CI 2015, and 4th InternationalWorkshop on NextGeneration of System Assurance Approaches for Safety-Critical Systems SASSUR, 2015

Y2 - 22 September 2015 through 22 September 2015

ER -

Becker M, Neumair M, Söhn A, Chakraborty S. Approaches for software verification of an emergency recovery system for Micro Air Vehicles. In van Gulijk C, Koornneef F, editors, Computer Safety, Reliability, and Security - AFECOMP 2015 Workshops ASSURE, DECSoS, ISSE, ReSA4CI, and SASSUR, Proceedings. Springer Verlag. 2015. p. 369-385. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-24249-1_32

Approaches for software verification of an emergency recovery system for Micro Air Vehicles

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this