Abstract
In this paper, we present a novel approach that seamlessly integrates requirements-based testing and model checking. Given a set of functional requirements and properties, both generic attributes and application specific constraints, expressed in our CLEAR requirements notation, our approach and the associated tool suite simultaneously generates an extensive set of requirements-based test cases using equivalence classes and synthesizes requirement models. The synthesized models support formal analysis of the properties using state-of-the-art model checkers that serves as a rigorous evidence of the quality and adequacy of the requirements. Further, the result of executing the test cases generated from those high-quality requirements on the implementation, helps ensure that those requirements are indeed met in the implementation. This comprehensive requirements-based approach to verification leverages automation and reduces defects in evidence generation for design assurance as outlined in guidance such as DO-178C and DO-333. We use the ArduCopter, an open-source platform, to illustrate our approach.
Supported by DARPA under agreement number FA8750-20-C-0226. The views, opinions and/or findings expressed are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.
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
Similar content being viewed by others
References
ArduPilot. https://ardupilot.org/ (2020)
Badger, J., Throop, D., Claunch, C.: Vared: verification and analysis of requirements and early designs. In: 2014 IEEE 22nd International Requirements Engineering Conference (RE), pp. 325–326 (2014). https://doi.org/10.1109/RE.2014.6912279
Bhatt, D., Chattopadhyay, A., Li, W., Oglesby, D., Owre, S., Shankar, N.: Contract-based verification of complex time-dependent behaviors in avionic systems. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 34–40. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_3
Bhatt, D., et al.: Constrained Language Enhanced Approach to Requirements (CLEAR) Requirements-Driven Model Checking and Test Generation 19 User Guide. Technical report, Honeywell International, ARCOS Program Tech Report, August 2021
Bhatt, D., Madl, G., Oglesby, D.: System architecture driven software design analysis methodology and toolset. Technical report, SAE Technical Paper (2012)
Bhatt, D., Madl, G., Oglesby, D., Schloegel, K.: Towards scalable verification of commercial avionics software. In: Proceedings of the AIAA Infotech@ Aerospace Conference (2010)
Bhatt, D., Murugesan, A., Hall, B., Ren, H., Jeppu, Y.: The clear way to transparent formal methods. In: 4th Workshop on Formal Integrated Development Environment - FLoC 2018 (2018)
Certification Authorities Software Team (CAST) and others: rationale for accepting masking MC/DC in certification projects. Position Paper 6, Technical report (2001)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_44
Conrad, E., Titolo, L., Giannakopoulou, D., Pressburger, T., Dutle, A.: A compositional proof framework for FRETish requirements (2022)
Crapo, A., Moitra, A., McMillan, C., Russell, D.: Requirements capture and analysis in assert (tm). In: 2017 IEEE 25th International Requirements Engineering Conference (RE), pp. 283–291. IEEE (2017)
Dutertre, B., Jovanovic, D., Navas, J.: Advanced symbolic analysis tools for fault-tolerant integrated distributed systems. NASA/CR-2018-21934, May 2018
Dutertre, B., Jovanović, D., Navas, J.A.: Verification of fault-tolerant protocols with sally. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 113–120. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-77935-5_8
Fifarek, A.W., Wagner, L.G., Hoffman, J.A., Rodes, B.D., Aiello, M.A., Davis, J.A.: SpeAR v2.0: formalized past LTL specification and analysis of requirements. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 420–426. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_30
Fuxman, A., Liu, L., Mylopoulos, J., Pistore, M., Roveri, M., Traverso, P.: Specifying and analyzing early requirements in tropos. Requirements Eng. 9(2), 132–150 (2004)
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language lustre. Proc. IEEE 79(9), 1305–1320 (1991)
Holzmann, G.J.: The model checker spin. IEEE Trans. Software Eng. 23(5), 279–295 (1997)
RTCA Inc.: RTCA DO-178C, Software Considerations in Airborne Systems and Equipment Certification (2011)
RTCA Inc.: RTCA DO-333, Formal Methods Supplement to DO-178C and DO-278A (2011)
SAE: ARP4754A: Guidelines for Development of Civil Aircraft and Systems. SAE International (2010)
Shankar, N., et al.: DesCert: design for certification, DARPA automated rapid certification of software (ARCOS), technical area 1 (TA-1), Phase 1 Report. Technical Report, SRI International (October 21 2021), provided upon request at https://github.com/SRI-CSL/DesCert/tree/master/Reports/Phase1Report
SRI International’s Computer Science Laboratory: Sally Model Checker. https://github.com/SRI-CSL/sally
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 This is a U.S. government work and not under copyright protection in the U.S.; foreign copyright protection may apply
About this paper
Cite this paper
Bhatt, D., Ren, H., Murugesan, A., Biatek, J., Varadarajan, S., Shankar, N. (2022). Requirements-Driven Model Checking and Test Generation for Comprehensive Verification. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds) NASA Formal Methods. NFM 2022. Lecture Notes in Computer Science, vol 13260. Springer, Cham. https://doi.org/10.1007/978-3-031-06773-0_31
Download citation
DOI: https://doi.org/10.1007/978-3-031-06773-0_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-06772-3
Online ISBN: 978-3-031-06773-0
eBook Packages: Computer ScienceComputer Science (R0)