Abstract
In this paper, we address the issue of safety-critical software verification and testing that are key requirements for achieving DO-331 and DO-178C regulatory compliance for airborne systems. Formal verification and testing are considered two different activities within the airborne standards and they belong to two different levels in avionics software development cycle. The objective is to integrate model-based verification and model-based testing within one framework and to capture the benefits of their cross-fertilization. It is achieved by proposing a methodology for the verification and testing of parallel communicating agents based on formal models. The results of formal verification and testing can be used as evidence for certification.
Sponsored by NSERC/CRD CMC CS Canada. Project CRIAQ AVIO 604, CRDPJ 463076-14.
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
References
http://www.rtca.org. RTCA/DO-178C: Software Considerations in Airborne Systems and Equipment Certification, Supplement to DO-178C and DO-278A: DO-332 Object-Oriented Technology and Related Techniques, DO-331 Model-Based Development and Verification, DO-333 Formal Methods (2011)
Zoughbi, G., Briand, L., Labiche, Y.: Modeling safety and airworthiness (RTCA DO-178B) information: conceptual model and UML profile. J. Softw. Syst. Model. 10(3), 337–367 (2011)
Moy, Y., Ledinot, E., Delseny, H., Wiels, V., Monate, B.: Testing or formal verification: DO-178C alternatives and industrial experience. J. IEEE Softw. 30(3), 50–57 (2013)
Peleska, J., Siegel, M.: Test automation of safety-critical reactive systems. S. Afr. Comput. J. 19, 53–77 (1997)
Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. MBT 2013, 3–28 (2013)
Yang, R., Chen, Z., Zhang, Z., Xu, B.: EFSM-based test case generation: sequence, data, and oracle. Int. J. Softw. Eng. Knowl. Eng. 25(4), 633–667 (2015)
Dssouli, R., Khoumsi, A., Elqortobi, M., Bentahar, J.: Testing the control-flow, data-flow, and time aspects of communication systems: a survey. Adv. Comput. 107, 95–155 (2017)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Massachusetts (1999)
Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1–18. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07512-9_1
El-Kholy, W., Bentahar, J., El-Menshawy, M., Qu, H., Dssouli, R.: Conditional commitments: reasoning and model checking. ACM Trans. Soft. Eng. Methodol. 24(2), 9:1–9:49 (2014)
Bourhfir, C., Aboulhamid, E., Dssouli, R., Rico, N.: A test case generation approach for conformance testing of SDL systems. Comput. Commun. 24(3–4), 319–333 (2001)
Bourhfir, C., Dssouli, R., Aboulhamid, E., Rico, N.: Automatic executable test case generation for extended finite state machine protocols. In: Kim, M., Kang, S., Hong, K. (eds.) Testing of Communicating Systems. ITIFIP, pp. 75–90. Springer, Boston, MA (1997). https://doi.org/10.1007/978-0-387-35198-8_6
Bourhfir, C., Dssouli, R., Aboulhamid, E., Rico, N.: A guided incremental test case generation procedure for conformance testing for CEFSM specified protocols. In: Petrenko, A., Yevtushenko, N. (eds.) Testing of Communicating Systems. ITIFIP, vol. 3, pp. 279–294. Springer, Boston, MA (1998). https://doi.org/10.1007/978-0-387-35381-4_17
Ammann, P.E., Black, P.E., Majurski. W.: Using model checking to generate tests from Specifications. In: Proceedings of the Second IEEE International Conference on Formal Engineering Methods (ICFEM 1998), pp. 46–54. IEEE Computer Society (1998)
Yin, X., Jiangyuan, Y., Wang, Z., Shi, X., Wu, J.: Modeling and testing of network protocols with parallel state machines. IEICE Trans. Inf. Syst. 98(12), 2091–2104 (2015)
Utting, M., Pretschner, A., Legeard, B.: A Taxonomy on Model-Based Testing. University of Waikato, Hamilton (2006)
Miller, S., Whalen, M., Cofer, D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010)
Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test., Verif. Reliabil. 19(3), 215–261 (2009)
Ouhammou, Y., et al.: A model-based process for the modelling and the analysis of avionic architectures. IJIIDS 10(1/2), 117–144 (2017)
Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundam. Inf. 26(3/4), 287–313 (1996)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Elqortobi, M., El-Khouly, W., Rahj, A., Bentahar, J., Dssouli, R. (2018). Model-Based Verification and Testing Methodology for Safety-Critical Airborne Systems. In: Abdelwahed, E., et al. New Trends in Model and Data Engineering. MEDI 2018. Communications in Computer and Information Science, vol 929. Springer, Cham. https://doi.org/10.1007/978-3-030-02852-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-02852-7_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02851-0
Online ISBN: 978-3-030-02852-7
eBook Packages: Computer ScienceComputer Science (R0)