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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Based on the number of DJI sales and their growing business figures over the last years. This is also supported by the number of and growth rate of registered MAVs at the federal agencies around Europe, and their estimated number of unreported vehicles [18].
- 2.
Heap was not used, and stack size was checked with Bound-T.
- 3.
A lower value is not possible, because all considered invocations are nondeterministic possibilities, and not enforced invocations.
References
The 2013 General Aviation Statistical Databook and 2014 Industry Outlook. Technical report, General Association of Aviation Manufacturers (2014)
Abzug, M., Larrabee, E.: Airplane Stability and Control, 2nd edn. Cambridge University Press, New York (2005)
Beyer, D.: Status report on software verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 373–388. Springer, Heidelberg (2014)
Bucur, D., Kwiatkowska, M.: On software verification for sensor nodes. J. Syst. Soft. 84(10), 1693–1707 (2011)
Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The Astreé analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012)
Dajiang Innovation Technology: DJI DropSafe (2014). http://www.dji.com/product/dropsafe. Accessed February 2015
Drone Technology: RPAS MCFLY-HELIOS (2015). http://www.dronetechnology.eu/rpas-mcfly-helios/. Accessed February 2015
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. Form. Methods Syst. Des. 35, 73–93 (2009)
Lattner, C.: LLVM and Clang: next generation compiler technology. In: The BSD Conference, pp. 1–2 (2008)
MARS Parachutes: M.A.R.S. 58 (2014). http://www.marsparachutes.com/mars-58/. Accessed January 2015
Mueller, M., D’Andrea, R.: Stability and control of a quadrocopter despite the complete loss of 1, 2, or 3 propellers. In: International Conference on Robotics and Automation (2014)
Opale Paramodels (2014). http://www.opale-paramodels.com/index.php/en/shop-opaleparamodels/rescue-systems. Accessed January 2015
Schlich, B., Kowalewski, S.: Model checking C source code for embedded systems. Int. J. Softw. Tools Technol. Transf. 11, 187–202 (2009)
Skycat: SKYCAT Parachute Launcher (2015). http://www.skycat.pro/tech-specs/. Accessed March 2015
Steer Davies Gleave: Study on the Third-Party Liability and Insurance Requirements of RPAS. Technical report, European Commission (2014)
Tidorum Ltd.: Bound-T time and stack analyzer (2015). http://www.bound-t.com/. Accessed January 2015
Wu, X., Wen, Y., Chen, L., Dong, W., Wang, J.: Data race detection for interrupt-driven programs via bounded model checking. In: 2013 IEEE Seventh International Conference on Software Security and Reliability Companion, pp. 204–210 (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Becker, M., Neumair, M., Söhn, A., Chakraborty, S. (2015). Approaches for Software Verification of An Emergency Recovery System for Micro Air Vehicles. In: Koornneef, F., van Gulijk, C. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2014. Lecture Notes in Computer Science(), vol 9338. Springer, Cham. https://doi.org/10.1007/978-3-319-24249-1_32
Download citation
DOI: https://doi.org/10.1007/978-3-319-24249-1_32
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24248-4
Online ISBN: 978-3-319-24249-1
eBook Packages: Computer ScienceComputer Science (R0)