Abstract
This paper describes a recent timed CTL (TCTL) model checker for Real-Time Maude. Our model checker is sound and complete for large classes of systems for which there were previously no TCTL model checkers. Furthermore, since Real-Time Maude also provides a formal analysis back-end to a number of modeling languages, our model checker also equips such languages with a TCTL model checker for free.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104, 2–34 (1993)
Bae, K., Ölveczky, P.C., Meseguer, J., Al-Nayeem, A.: The SynchAADL2Maude tool. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 59–62. Springer, Heidelberg (2012)
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)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)
Lepri, D., Ölveczky, P.C., Ábrahám, E.: Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories (submitted for publication, 2013), http://folk.uio.no/leprid/TCTL-RTM/
Lepri, D., Ábrahám, E., Ölveczky, P.C.: Timed CTL model checking in Real-Time Maude. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 182–200. Springer, Heidelberg (2012)
Markey, N., Schnoebelen, P.: TSMV: A symbolic model checker for quantitative analysis of systems. In: QEST 2004. IEEE Computer Society (2004)
Ö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)
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)
Ö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)
Wang, F.: Efficient verification of timed automata with BDD-like data structures. STTT 6(1), 77–97 (2004)
Yovine, S.: Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer 1(1-2), 123–133 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lepri, D., Ábrahám, E., Ölveczky, P.C. (2013). A Timed CTL Model Checker for Real-Time Maude. In: Heckel, R., Milius, S. (eds) Algebra and Coalgebra in Computer Science. CALCO 2013. Lecture Notes in Computer Science, vol 8089. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40206-7_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-40206-7_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40205-0
Online ISBN: 978-3-642-40206-7
eBook Packages: Computer ScienceComputer Science (R0)