Advertisement

Virtual Integration for Pattern-Based Contracts with the Kind2 Model Checker

  • Jan Steffen Becker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11119)

Abstract

In component based design of embedded software, virtual integration verifies hierarchical decomposition of components and contracts. In this paper we present a virtual integration analysis that is based on the Kind2 state-of-the-art model checker. Our method focuses on pattern-based requirements with automata-based semantics. We propose the Simplified Universal Pattern that is used in the BTC EmbeddedPlatform as a specification language, but other languages may be used as well. The main contribution is a reduction of virtual integration to a reachability problem on so-called counter automata that form the semantics of the pattern language. The counter automata are translated to the synchronous data flow language Lustre, that serves as input for Kind2. Kind2 turns out to be quite powerful in proving the safety properties that result from the reachability problem for the automata. Thus, it yields a positive sound (but not complete) verification technique that gives a sufficient condition for virtual integration.

Keywords

Contract-based design Formal methods Virtual integration Model checking Requirements engineering Verification 

References

  1. 1.
    Becker, J.S.: Analyzing consistency of formal requirements. In: Automated Verification of Critical Systems (AVOCS 2018) (2018)Google Scholar
  2. 2.
    Becker, J.S., et al.: Interoperable toolchain for requirements-driven model-based development. In: ERTS 2018 (2018)Google Scholar
  3. 3.
    Bensalem, S., Bozga, M., Nguyen, T.H., Sifakis, J.: Compositional verification for component-based systems and application. IET Software 4(3), 181–193 (2010)CrossRefGoogle Scholar
  4. 4.
    Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional verification for component-based systems and application. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 64–79. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-88387-6_7CrossRefzbMATHGoogle Scholar
  5. 5.
    Benveniste, A.: Contracts for system design. Found. Trends Electron. Design Autom. 12(2–3), 124–400 (2018)CrossRefGoogle Scholar
  6. 6.
    Bienmüller, T., Teige, T., Eggers, A., Stasch, M.: Modeling requirements for quantitative consistency analysis and automatic test case generation. In: FM&MDD 2016. Computing Science Technical report Series, vol. CS-TR-1503. Newcastle University (2016)Google Scholar
  7. 7.
    Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-18275-4_7CrossRefGoogle Scholar
  8. 8.
    Brat, G., Bushnell, D., Davies, M., Giannakopoulou, D., Howar, F., Kahsai, T.: Verifying the safety of a flight-critical system. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 308–324. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-19249-9_20CrossRefGoogle Scholar
  9. 9.
    Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: a mode-aware contract language for reactive systems. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 347–366. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41591-8_24CrossRefGoogle Scholar
  10. 10.
    Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering, pp. 702–705. IEEE Press (2013)Google Scholar
  11. 11.
    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).  https://doi.org/10.1007/978-3-642-28891-3_13CrossRefGoogle Scholar
  12. 12.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, pp. 411–420. ACM (1999)Google Scholar
  13. 13.
    Ellen, C., Sieverding, S., Hungar, H.: Detecting consistencies and inconsistencies of pattern-based functional requirements. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 155–169. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-10702-8_11CrossRefGoogle Scholar
  14. 14.
    Filipovikj, P., Jagerfield, T., Nyberg, M., Rodriguez-Navas, G., Seceleanu, C.: Integrating pattern-based formal requirements specification in an industrial tool-chain. In: 2016 IEEE 40th Annual Computer Software and Applications Conference (COMPSAC), vol. 2, pp. 167–173. IEEE (2016)Google Scholar
  15. 15.
    Gezgin, T., Oertel, M., Weber, R.: Multi-aspect virtual integration approach for real-time and safety properties. In: International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS 2014). IEEE, October 2014Google Scholar
  16. 16.
    Jahier, E., Raymond, P., Halbwachs, N.: The Lustre V6 Reference Manual. IMAG, December 2016Google Scholar
  17. 17.
    Jeannet, B., Gaucher, F.: Debugging embedded systems requirements with stimulus: an automotive case-study. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016) (2016)Google Scholar
  18. 18.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  19. 19.
    Project TIMMO: TIMMO Partners: TADL: Timing augmented description language version 2. Deliverable d6, The TIMMO Consortium, October 2009Google Scholar
  20. 20.
    Reinkemeier, P., Stierand, I., Rehkop, P., Henkler, S.: A pattern-based requirement specification language: mapping automotive specific timing requirements. In: Software Engineering (Workshops), vol. 184, pp. 99–108 (2011)Google Scholar
  21. 21.
    Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-Solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127–144. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-40922-X_8CrossRefGoogle Scholar
  22. 22.
    Teige, T.: Simplified Universal Pattern Syntax and Semantics. BTC Embedded Systems, June 2017. ConfidentialGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.OFFIS e.V. Institute for Information TechnologyOldenburgGermany

Personalised recommendations