Skip to main content
SpringerLink
Log in

Timed CTL Model Checking in Real-Time Maude

  • Conference paper
Rewriting Logic and Its Applications (WRLA 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7571))

Included in the following conference series:

Abstract

This paper presents a timed CTL model checker for Real- Time Maude and its semantic foundations. In particular, we give a timed CTL model checking procedure for that is sound and complete for closedbound formulas under a continuous semantics for a fairly large class of systems. An important benefit of our model checker is that it also automatically provides a timed CTL model checker for subsets of modeling languages, like Ptolemy II and (Synchronous) AADL, which have Real- Time Maude model checking integrated into their tool environments.

This work was partially supported by the Research Council of Norway through the Rhytm project, by the DAADppp HySmart project, and by AFOSR Grant FA8750- 11-2-0084.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. van der Aalst, W.M.P.: Interval Timed Coloured Petri Nets and their Analysis. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 453–472. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  2. AlTurki, M., Meseguer, J.: Real-time rewriting semantics of Orc. In: Proc. PPDP 2007. ACM (2007)

    Google Scholar 

  3. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  4. Alur, R., Henzinger, T.: Logics and Models of Real Time: A Survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  5. Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104, 2–34 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bae, K., Ölveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and Its Formal Analysis in Real-Time Maude. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 651–667. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Bae, K., Ölveczky, P.C., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. Science of Computer Programming (to appear, 2012), doi:10.1016/j.scico.2010.10.002

    Google Scholar 

  8. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)

    Google Scholar 

  9. Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Boronat, A., Ölveczky, P.C.: Formal Real-Time Model Transformations in MOMENT2. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 29–43. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Boucheneb, H., Gardey, G., Roux, O.H.: TCTL Model Checking of Time Petri Nets. J. Logic Computation 19(6), 1509–1540 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  12. Bouyer, P.: Model-checking timed temporal logics. ENTCS 231, 323–341 (2009)

    MathSciNet  Google Scholar 

  13. Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: DAC 1995 (1995)

    Google Scholar 

  14. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  15. Eker, J., Janneck, J.W., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity—the Ptolemy approach. Proceedings of the IEEE 91(2), 127–144 (2003)

    Article  Google Scholar 

  16. Gardey, G., Lime, D., Magnin, M., Roux, O.(H.): Romeo: A Tool for Analyzing Time Petri Nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  17. Katelman, M., Meseguer, J., Hou, J.: Redesign of the LMST Wireless Sensor Protocol through Formal Modeling and Statistical Model Checking. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 150–169. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Laroussinie, F., Markey, N., Schnoebelen, P.: Efficient timed model checking for discrete-time systems. Theor. Comput. Sci. 353, 249–271 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  19. Lepri, D., Ölveczky, P.C., Ábrahám, E.: Timed CTL model checking in Real-Time Maude, http://folk.uio.no/leprid/TCTL-RTM/tctl-rtm2011.pdf

  20. Lepri, D., Ölveczky, P.C., Ábrahám, E.: Model checking classes of metric LTL properties of object-oriented Real-Time Maude specifications. In: Proc. RTRTS 2010. EPTCS, vol. 36, pp. 117–136 (2010)

    Google Scholar 

  21. Lien, E., Ölveczky, P.C.: Formal modeling and analysis of an IETF multicast protocol. In: Proc. SEFM 2009. IEEE Computer Society (2009)

    Google Scholar 

  22. Markey, N., Schnoebelen, P.: TSMV: A Symbolic Model Checker for Quantitative Analysis of Systems. In: QEST. IEEE Computer Society (2004)

    Google Scholar 

  23. Morasca, S., Pezzè, M., Trubian, M.: Timed high-level nets. The Journal of Real-Time Systems 3, 165–189 (1991)

    Article  Google Scholar 

  24. Ölveczky, P.C.: Semantics, Simulation, and Formal Analysis of Modeling Languages for Embedded Systems in Real-Time Maude. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 368–402. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  25. Ölveczky, P.C., Boronat, A., Meseguer, J.: Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude. In: Hatcliff, J., Zucca, E. (eds.) FMOODS/FORTE 2010, Part II. LNCS, vol. 6117, pp. 47–62. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  26. Ölveczky, P.C., Caccamo, M.: Formal Simulation and Analysis of the CASH Scheduling Algorithm in Real-Time Maude. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 357–372. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  27. Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science 285, 359–405 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  28. Ölveczky, P.C., Meseguer, J.: Abstraction and completeness for Real-Time Maude. Electronic Notes in Theoretical Computer Science 176(4), 5–27 (2007)

    Article  Google Scholar 

  29. Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)

    Article  MATH  Google Scholar 

  30. Ölveczky, P.C., Meseguer, J.: The Real-Time Maude Tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332–336. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  31. Ölveczky, P.C., Meseguer, J., Talcott, C.L.: Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. Formal Methods in System Design 29(3), 253–293 (2006)

    Article  MATH  Google Scholar 

  32. Ölveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude. Theoretical Computer Science 410(2-3), 254–280 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  33. Riesco, A., Verdejo, A.: Implementing and analyzing in Maude the enhanced interior gateway routing protocol. Electr. Notes Theor. Comput. Sci. 238(3), 249–266 (2009)

    Article  Google Scholar 

  34. Rivera, J.E., Durán, F., Vallecillo, A.: On the Behavioral Semantics of Real-Time Domain Specific Visual Languages. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 174–190. Springer, Heidelberg (2010), see also the e-Motions web page http://atenea.lcc.uma.es/index.php/Main_Page/Resources/E-motions

    Chapter  Google Scholar 

  35. Wang, F.: Formal verification of timed systems: A survey and perspective. Proceedings of the IEEE 92(8), 1283–1307 (2004)

    Article  Google Scholar 

  36. Wang, F.: REDLIB for the formal verification of embedded systems. In: Proc. ISoLA 2006. IEEE (2006)

    Google Scholar 

  37. Wirsing, M., Bauer, S.S., Schroeder, A.: Modeling and analyzing adaptive user-centric systems in Real-Time Maude. In: Proc. RTRTS 2010. EPTCS, vol. 36, pp. 1–25 (2010)

    Google Scholar 

  38. Yovine, S.: Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer 1(1-2), 123–133 (1997)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oslo, Norway

    Daniela Lepri & Peter Csaba Ölveczky

  2. RWTH Aachen University, Germany

    Erika Ábrahám

  3. University of Illinois at Urbana-Champaign, USA

    Peter Csaba Ölveczky

Authors
  1. Daniela Lepri
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Erika Ábrahám
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Csaba Ölveczky
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Lenguajes y Ciencias de la Computacíon, E.T.S.I Informática, Universidad de Málaga, Boulevard Louis Pasteur, s/n, Campus de Teatinos, 29071, Málaga, Spain

    Franciso Durán

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lepri, D., Ábrahám, E., Ölveczky, P.C. (2012). Timed CTL Model Checking in Real-Time Maude. In: Durán, F. (eds) Rewriting Logic and Its Applications. WRLA 2012. Lecture Notes in Computer Science, vol 7571. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34005-5_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-34005-5_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-34004-8

  • Online ISBN: 978-3-642-34005-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation