From Design Contracts to Component Requirements Verification

  • Jing LiuEmail author
  • John D. Backes
  • Darren Cofer
  • Andrew Gacek
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9690)


During the development and verification of complex airborne systems, a variety of languages and development environments are used for different levels of the system hierarchy. As a result, there may be manual steps to translate requirements between these different environments. This paper presents a tool-supported export technique that translates high-level requirements from the software architecture modeling environment into observers of requirements that can be used for verification in the software component environment. This allows efficient verification that the component designs comply with their high-level requirements. It also provides an automated tool chain supporting formal verification from system requirements down to low-level software requirements that is consistent with certification guidance for avionics systems. The effectiveness of the technique has been evaluated and demonstrated on a medical infusion pump and an aircraft wheel braking system.


Design contracts Specification model Design model AGREE Simulink Requirements-based verification Certification 



This work was funded by NASA under contract NNA13AA21C (Compositional Verification of Flight Critical Systems). We would like to thank Chad Van Fleet, Anitha Murugesan, and Mike Whalen for their valuable feedback during this work.


  1. 1.
    Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126–140. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  2. 2.
    Whalen, M.W., Gacek, A., Cofer, D.D., Murugesan, A., Heimdahl, M.P.E., Rayadurgam, S.: Your “what” is my “how”: Iteration and hierarchy in system design. IEEE Softw. 30, 54–60 (2013)CrossRefGoogle Scholar
  3. 3.
    Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language, 1st edn. Addison-Wesley Professional, Boston (2012)Google Scholar
  4. 4.
    MathWorks: Simulink (2016).
  5. 5.
    RTCA DO-178C: Software Considerations in Airborne Systems and Equipment Certification, Washington, DC (2011)Google Scholar
  6. 6.
    RTCA DO-333: Formal Methods Supplement to DO-178C and DO-278A, Washington, DC (2011)Google Scholar
  7. 7.
    RTCA DO-331: Model-Based Development and Verification Supplement to DO-178C and DO-278A, Washington, DC (2011)Google Scholar
  8. 8.
    Cofer, D., Miller, S.P.: Formal methods case studies for DO-333, NASA contractor report NASA/CR-2014-218244 (2014)Google Scholar
  9. 9.
  10. 10.
    Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl, M.P.: Compositional verification of a medical device system. In: ACM International Conference on High Integrity Language Technology (HILT) 2013. ACM (2013)Google Scholar
  11. 11.
    Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language LUSTRE. Proc. IEEE 79, 1305–1320 (1991)CrossRefGoogle Scholar
  12. 12.
    Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edn. Cambridge University Press, Cambridge (2004)CrossRefzbMATHGoogle Scholar
  13. 13.
    Backes, J., et al.: AGREE toolset (2016).
  14. 14.
    RTCA DO-330: Software Tool Qualification Considerations, Washington, DC (2011)Google Scholar
  15. 15.
    Miller, S.P., Bhattacharyya, S., Tinelli, C., Smolka, S., Sticksel, C., Meng, B., Yang, J.: Formal verification of quasi-synchronous systems. Final Technical report delivered Air Force Research Laboratory (2015)Google Scholar
  16. 16.
    Accident, C.A., Incident Investigation Commission (CIAIAC), S.: Technical report: Accident occurred on 21 May 1998 to Aircraft Airbus A-320-21 Registration G-UKLL At Ibiza Airport, Balearic Islands (1998)Google Scholar
  17. 17.
    CriSys Group: Generic patient controlled analgesia infusion pump project (2016).
  18. 18.
    Wang, C., Pastore, F., Goknil, A., Briand, L., Iqbal, Z.: Automatic generation of system test cases from use case specifications. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, pp. 385–396. ACM, New York (2015)Google Scholar
  19. 19.
    Ibrahim, R., Saringat, M., Ibrahim, N., Ismail, N.: An automatic tool for generating test cases from the system’s requirements. In: 7th IEEE International Conference on Computer and Information Technology, CIT 2007, pp. 861–866 (2007)Google Scholar
  20. 20.
    Escalona, M.J., Gutierrez, J.J., Mejías, M., Aragón, G., Ramos, I., Torres, J., Domínguez, F.J.: An overview on test generation from functional requirements. J. Syst. Softw. 84, 1379–1393 (2011)CrossRefGoogle Scholar
  21. 21.
    Miller, S.P., Tribble, A.C., Whalen, M.W., Heimdahl, M.P.E.: Proving the shalls: early validation of requirements through formal methods. Int. J. Softw. Tools Technol. Transf. 8, 303–319 (2006)CrossRefGoogle Scholar
  22. 22.
    Bozzano, M., Cimatti, A., Katoen, J., Katsaros, P., Mokos, K., Nguyen, V.Y., Noll, T., Postma, B., Roveri, M.: Spacecraft early design validation using formal methods. Reliab. Eng. Syst. Saf. 132, 20–35 (2014)CrossRefGoogle Scholar
  23. 23.
    Silva, W., Bezerra, E., Winterholer, M., Lettnin, D.: Automatic property generation for formal verification applied to hdl-based design of an on-board computer for space applications. In: 2013 14th Latin American Test Workshop (LATW), pp. 1–6 (2013)Google Scholar
  24. 24.
    Soeken, M., Kuhne, U., Freibothe, M., Fe, G., Drechsler, R.: Automatic property generation for the formal verification of bus bridges. In: 2011 IEEE 14th International Symposium on Design and Diagnostics of Electronic Circuits Systems (DDECS), pp. 417–422 (2011)Google Scholar
  25. 25.
    Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. Part 3 97, 333–348 (2015)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Jing Liu
    • 1
    Email author
  • John D. Backes
    • 2
  • Darren Cofer
    • 2
  • Andrew Gacek
    • 2
  1. 1.Advanced Technology Center, Rockwell CollinsCedar RapidsUSA
  2. 2.Advanced Technology Center, Rockwell CollinsMinneapolisUSA

Personalised recommendations