This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Practical Uses of Formal Methods in Development of Airborne Software
Technical Paper
2016-01-2044
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
Over the past few decades, advanced methods have been developed for the analysis of digital systems using mathematical reasoning, i.e., formal logic. These methods are supported by sophisticated software tools that can be used to perform analysis far beyond what is practically achievable using “paper and pencil” analysis. In December 2011, RTCA published RTCA DO-178C [1] along with a set of technical supplements including RTCA DO-333 [2] which provides guidance on the use of formal methods towards the certification of airborne software. Such methods have the potential to reduce the cost of verification by using formal analysis instead of conventional test-based methods to produce a portion of the verification evidence required for certification. Formal methods can also be used to find problems earlier in the development process - for example, while the requirements are being developed rather than during system integration when the cost of re-working the requirements and design is much higher. This paper provides an introduction to the practical use of formal methods in the development and certification of airborne software. The paper includes an illustrative example of using formal methods motivated by experience with the application of formal methods to engine control software.
Recommended Content
Authors
Citation
Joyce, J., Beecher, S., Fabre, L., and Rajagopalan, R., "Practical Uses of Formal Methods in Development of Airborne Software," SAE Technical Paper 2016-01-2044, 2016, https://doi.org/10.4271/2016-01-2044.Also In
References
- RTCA DO-178 Software Considerations in Airborne Systems and Equipment Certification RTCA and EUROCAE 2011
- RTCA DO-333 Formal Methods Supplement to DO-178C and DO-278A RTCA and EUROCAE 2011
- Moy Y. , Ledinot E. , Delseny H. , Wiels V. , and Monate B. Testing or Formal Verification: DO-178C Alternatives and Industrial Experience IEEE Software 30 3 50 57 May June 2013
- NuSMV homepage http://nusmv.fbk.eu/
- Miller S. , Whalen M. , and Cofer D. Software model checking takes off Commun. ACM 53 2 58 64 February 2010