A Methodology for Formal Requirements Validation and Automatic Test Generation and Application to Aerospace Systems
Published October 30, 2018 by SAE International in United States
Downloadable datasets for this paper availableAnnotation of this paper is available
Automation on Validation and Verification (V&V) leveraging Formal Methods, and in particular Model Checking, is seeing an increasing use in the Aerospace domain. In recent years, Formal Methods have been used to verify systems and software and its correctness as a way to augment traditional methods relying on simulation and testing. Recent updates to the relevant Aerospace regulations (e.g. DO178C, DO331 and DO333) now have explicit provisions for utilization of models and formal methods. In a previous paper a compositional methodology for the verification of Aerospace Systems has been described with application to Electrical Power Generation and Distribution Systems. In this paper we present an expansion of the previous work in two directions. First, we describe the application of the methodology to the validation of Proximity Sensing Systems (PSS) requirements showing the effectiveness of the method to a new aerospace domain. Second, both the methodology and technology components have been expanded and applied to the PSS to enable automatic generation of test cases from the validated requirements models showing a novel application of formal models in an integrated process and toolset in new areas of application in the context of the Aerospace Domain.
CitationFerrante, O., Scholte, E., Rollini, S., North, R. et al., "A Methodology for Formal Requirements Validation and Automatic Test Generation and Application to Aerospace Systems," SAE Technical Paper 2018-01-1948, 2018, https://doi.org/10.4271/2018-01-1948.
Data Sets - Support Documents
|[Unnamed Dataset 1]|
|[Unnamed Dataset 2]|
|[Unnamed Dataset 3]|
|[Unnamed Dataset 4]|
- Cofer, D. , “Formal Methods in the Aerospace Industry: Follow the Money,” Proceedings 14th International Conference on Formal Engineering Methods: Formal Methods and Software Engineering (ICFEM) 2012. Kyoto, Japan, 2012, doi:10.1007/978-3-642-34281-3_2.
- Holloway, C.M. and Hayhurst, K.J. , “Challenges in Software Aspects of Aerospace Systems,” Proceedings 26th Annual NASA Goddard Software Engineering Workshop (SEW), Greenbelt, MD, 2002, 1-7, doi:10.1109/SEW.2001.992649
- Ferrante, O., Scholte, E., Pinello, C., Ferrari, A. et al. , “A Methodology for Increasing the Efficiency and Coverage of Model Checking and its Application to Aerospace Systems,” SAE Int. J. Aerosp. 9(1):140-150, 2016, doi:10.4271/2016-01-2053.
- Miller, S.P., Whalen, M.W., and Cofer, D.D. , “Software Model Checking Takes Off,” Communications of the ACM 53(2), 2010.
- Clarke, E., Grumberg, O., Peleg, D. , Model Checking (Dec. 1999).
- RTCA DO-331 , “Model-Based Development and Verification Supplement to DO-178C and DO-278A,” 2011.
- Myers, G. , The Art of Software Testing (John Wiley & Sons, 1979).
- RTCA , DO-178C Standard “Software Considerations in Airborne Systems and Equipment Certification,” 2011
- Chilenski, J. and Miller, S. , “Applicability of Modified Condition/Decision Coverage to Software Testing,” Soft. Eng. J. 9(5):193-200, 1994.
- Chilenski, J. , “An Investigation of Three Forms of the Modified Condition Decision Coverage (MCDC) Criterion,” Technical Report, DOT/FAA/AR-01/18, 2001
- Hayhurst, K., Veerhusen, D., Chilenski, J., and Rierson, L. , “A Practical Tutorial on Modified Condition/Decision Coverage,” Technical Report NASA/TM-2001-210876, 2001.
- Fraser, G., Wotawa, F., and Amman, P.E. , “Testing with Model Checkers: A Survey,” Soft. Test. Verif. Reliab. 19:215-261, 2009.
- Enoiu, E.P., Čaušević, A., Ostrand, T.J. et al. , “Automated Test Generation Using Model Checking: An Industrial Evaluation,” Int. J. Softw. Tools Technol. Transfer 18:335, 2016.
- Bennion, M. and Habli, I. , “A Candid Industrial Evaluation of Formal Software Verification Using Model Checking,” ICSE Companion 175-184, 2014.
- Bochot, T., Virelizier, P., Waeselynck, H., and Wiels, V. , “Model Checking Flight Control Systems: The Airbus Experience,” Proceedings 31st International Conference on Software Engineering, Vancouver, BC, Canada, 2009, 18-27, doi:10.1109/ICSE-COMPANION.2009.5070960
- RTCA DO-330 , “Software Tool Qualification Considerations Supplement to DO-178C and DO-278A,” 2011.