Compositional verification of real-time systems using Ecdar | International Journal on Software Tools for Technology Transfer Skip to main content
Springer Nature Link
Log in

Compositional verification of real-time systems using Ecdar

  • MTM
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

We present a specification theory for timed systems implemented in the Ecdar tool. We illustrate the operations of the specification theory on a running example, showing the models and verification checks. To demonstrate the power of the compositional verification, we perform an in depth case study of a leader election protocol; Modeling it in Ecdar as Timed input/output automata Specifications and performing both monolithic and compositional verification of two interesting properties on it. We compare the execution time of the compositional to the classical verification showing a huge difference in favor of compositional verification.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abadi M., Lamport L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993)

    Article  Google Scholar 

  2. Alur R., Dill D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: CONCUR’98. LNCS, vol. 1466. Springer, Berlin (1998)

  4. Andersen H.R., Winskel G.: Compositional checking of satisfaction. In: Larsen, K.G., Skou, A. (eds.) CAV. Lecture Notes in Computer Science, vol. 575, pp. 24–36. Springer, Berlin (1991)

    Google Scholar 

  5. Baeten J.C.M.: A brief history of process algebra. Theor. Comput. Sci. 335(2–3), 131–146 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  6. Barnett, M., Rustan, K., Leino, M., Schulte, W.: The Spec# programming system: an overview. In: CASSIS 2004. LNCS, vol. 3362. Springer, Berlin (2004)

  7. Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: Uppaal-tiga: time for playing games! In: CAV. LNCS, vol. 4590. Springer, Berlin (2007)

  8. Bulychev, P., Chatain, T., David, A., Larsen, K.G.: Efficient on-the-fly algorithm for checking alternating timed simulation. In: FORMATS. LNCS, vol. 5813, pp. 73–87. Springer, Berlin (2009)

  9. Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Legay, A.: Distributed parametric and statistical model checking. In: Barnat, J., Heljanko, K. (eds.) PDMC. EPTCS, vol. 72, pp. 30–42 (2011)

  10. Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: CONCUR (2005)

  11. David A., Larsen K.G., Legay A., Mikucionis M., Poulsen D.B., van Vliet J., Wang Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS. Lecture Notes in Computer Science, vol. 6919, pp. 80–96. Springer, Berlin (2011)

    Google Scholar 

  12. David A., Larsen K.G., Legay A., Mikucionis M., Wang Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. Lecture Notes in Computer Science, vol. 6806, pp. 349–355. Springer, Berlin (2011)

    Google Scholar 

  13. David A., Larsen K.G., Legay A., Nyman U., Wasowski A.: Timed i/o automata: a complete specification theory for real-time systems. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp. 91–100. ACM, New York (2010)

    Chapter  Google Scholar 

  14. de Alfaro, L., Henzinger, T.A.: Interface automata. In: FSE, Vienna, Austria, September 2001. pp. 109–120. ACM Press, New York

  15. de Alfaro, L., Henzinger, T.A.: Interface-based design. In: In Engineering Theories of Software Intensive Systems, Marktoberdorf Summer School. Kluwer Academic Publishers, Dordrecht (2004)

  16. de Alfaro L., Henzinger T.A., Stoelinga M.I.A.: Timed interfaces. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT. LNCS, vol. 2491, pp. 108–122. Springer, Berlin (2002)

    Google Scholar 

  17. De Nicola, R., Segala, R.: A process algebraic view of input/output automata. Theor. Comput. Sci. 138 (1995)

  18. Fahrenberg U., Legay A., Wasowski A.: Vision paper: make a difference! (semantically). In: Whittle, J., Clark, T., Kühne, T. (eds.) MoDELS. Lecture Notes in Computer Science, vol. 6981, pp. 490–500. Springer, Berlin (2011)

    Google Scholar 

  19. Floyd R.W.: Assigning meanings to programs. Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19, 19–31 (1967)

    MathSciNet  Google Scholar 

  20. Garland, S.J., Lynch, N.A.: The IOA language and toolset: support for designing, analyzing, and building distributed systems. Technical report, Massachusetts Institute of Technology, Cambridge (1998)

  21. Hoare C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  22. Hoare C.A.R., He J.: The weakest prespecification. Inf. Process. Lett. 24, 127–132 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  23. Hoare C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice Hall, Upper Saddle River (1985)

    Google Scholar 

  24. Jones C.B.: Specification as a design base (extended abstract). In: Duijvestijn, A.J.W., Lockemann, P.C. (eds.) ECI. Lecture Notes in Computer Science, vol. 123, pp. 103–105. Springer, Berlin (1981)

    Google Scholar 

  25. Jones C.B.: Systematic Software Development using VDM. Series in Computer Science. Prentice-Hall, Upper Saddle River (1986)

    Google Scholar 

  26. Kaynar, D.K., Lynch, N.A., Segala, R., Vaandrager, F.W.: Timed i/o automata: A mathematical framework for modeling and analyzing real-time systems. In: RTSS, pp. 166–177. IEEE Computer Society, New York (2003)

  27. Larsen, K.G.: Context-Dependent Bisimulation Between Processes. PhD thesis, Department of Computer Science, University of Edinburgh (1986)

  28. Larsen K.G., Xinxin L.: Compositionality through an operational semantics of contexts. In: Paterson, M. (ed.) ICALP. Lecture Notes in Computer Science, vol. 443, pp. 526–539. Springer, Berlin (1990)

    Google Scholar 

  29. Leavens G.T., Baker A.L.: Enhancing the pre- and postcondition technique for more expressive specifications. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM’99—Formal Methods: World Congress on Formal Methods in Development of Computer Systems. Lecture Notes in Computer Science, vol. 1709, pp. 1087–1106. Springer, Berlin (1999)

    Google Scholar 

  30. Lynch, N.: I/O automata: a model for discrete event systems. In: Annual Conference on Information Sciences and Systems, pp. 29–38. Princeton University, Princeton (1988)

  31. Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. Technical Report MIT/LCS/TM-373. The MIT Press, Cambridge (1988)

  32. Owicki S.S., Gries D.: An axiomatic proof technique for parallel programs i. Acta Inf. 6, 319–340 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  33. Stark, E.W., Cleavland, R., Smolka, S.A.: A process-algebraic language for probabilistic I/O automata. In: CONCUR. LNCS, pp. 189–203. Springer, Berlin (2003)

  34. Sun, J., Liu, Y., Dong, J.S.: Model checking csp revisited: Introducing a process analysis toolkit. In: Proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008). Communications in Computer and Information Science, vol. 17, pp. 307–322. Springer, Berlin (2008)

  35. Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Etienne, A.: Modeling and verifying hierarchical real-time systems using stateful timed csp. ACM Trans. Softw. Eng. Methodol. (2012, Accepted)

  36. Szyperski C.: Component Software, Beyond Object-Oriented Programming. Addison-Wesley, Boston (1997)

    Google Scholar 

  37. Vaandrager, F.W.: On the relationship between process algebra and input/output automata. In: LICS. pp. 387–398 (1991)

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Aalborg, Denmark

    Alexandre David, Kim. G. Larsen, Mikael H. Møller, Ulrik Nyman, Anders P. Ravn & Arne Skou

  2. INRIA/IRISA, Rennes Cedex, France

    Axel Legay

  3. IT University of Copenhagen, Copenhagen, Denmark

    Andrzej Wąsowski

Authors
  1. Alexandre David
    View author publications

    You can also search for this author inPubMed Google Scholar

  2. Kim. G. Larsen
    View author publications

    You can also search for this author inPubMed Google Scholar

  3. Axel Legay
    View author publications

    You can also search for this author inPubMed Google Scholar

  4. Mikael H. Møller
    View author publications

    You can also search for this author inPubMed Google Scholar

  5. Ulrik Nyman
    View author publications

    You can also search for this author inPubMed Google Scholar

  6. Anders P. Ravn
    View author publications

    You can also search for this author inPubMed Google Scholar

  7. Arne Skou
    View author publications

    You can also search for this author inPubMed Google Scholar

  8. Andrzej Wąsowski
    View author publications

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence to Ulrik Nyman.

Additional information

Authors of this paper has been supported by MT-LAB, A VKR Centre of Excellence in Modeling of IT, and the Sino-Danish Basic Research Center IDEA4CPS.

Rights and permissions

Reprints and permissions

About this article

Cite this article

David, A., Larsen, K.G., Legay, A. et al. Compositional verification of real-time systems using Ecdar . Int J Softw Tools Technol Transfer 14, 703–720 (2012). https://doi.org/10.1007/s10009-012-0237-y

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-012-0237-y

Keywords