This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
A Methodology for Formal Requirements Validation and Automatic Test Generation and Application to Aerospace Systems
Technical Paper
2018-01-1948
ISSN: 0148-7191, e-ISSN: 2688-3627
This content contains downloadable datasets
Annotation ability available
Sector:
Language:
English
Abstract
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.
Recommended Content
Authors
Topic
Citation
Ferrante, 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
Title | Description | Download |
---|---|---|
Unnamed Dataset 1 | ||
Unnamed Dataset 2 | ||
Unnamed Dataset 3 | ||
Unnamed Dataset 4 |
Also In
References
- 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 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 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 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 1999
- RTCA DO-331 2011
- https://www.reactive-systems.com/
- https://www.mathworks.com/products/sldesignverifier/features.html
- Myers , G. The Art of Software Testing John Wiley & Sons 1979
- RTCA 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. 2001
- Hayhurst , K. , Veerhusen , D. , Chilenski , J. , and Rierson , L. 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. 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 10.1109/ICSE-COMPANION.2009.5070960
- RTCA DO-330 2011
- https://www.mathworks.com/products/polyspace-code-prover/features.html