{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T06:29:37Z","timestamp":1790749777128,"version":"4.1.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2007,2,24]],"date-time":"2007-02-24T00:00:00Z","timestamp":1172275200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2007,4,4]]},"DOI":"10.1007\/s10990-007-9001-5","type":"journal-article","created":{"date-parts":[[2007,2,24]],"date-time":"2007-02-24T03:23:37Z","timestamp":1172287417000},"page":"161-196","source":"Crossref","is-referenced-by-count":193,"title":["Semantics and pragmatics of Real-Time Maude"],"prefix":"10.1007","volume":"20","author":[{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,2,24]]},"reference":[{"key":"9001_CR1","doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P.: Interval timed coloured Petri nets and their analysis. In: Marsan M.A. (ed.) Application and Theory of Petri Nets 1993, vol. 691 of Lecture Notes in Computer Science, pp. 453\u2013472. Springer (1993)","DOI":"10.1007\/3-540-56863-8_61"},{"key":"9001_CR2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"9001_CR3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"1262","author":"R. Alur","year":"1994","unstructured":"Alur R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"9001_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Logics and models of real time: A survey. In: de Bakker, J.W., Huizing, K., de Roever, W.-P., Rozenberg, G. (eds.) Real Time: Theory in Practice, vol. 600 of Lecture Notes in Computer Science, pp. 74\u2013106. Springer (1992)","DOI":"10.1007\/BFb0031988"},{"key":"9001_CR5","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) Proc. Formal Methods for the Design of Real-Time Systems (SFM-RT 2004), vol. 3185 of Lecture Notes in Computer Science, pp. 200\u2013236. Springer (2004) See also Uppaal home page at http:\/\/www.uppaal.com","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"9001_CR6","doi-asserted-by":"crossref","unstructured":"Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J.: Tools and applications II: The IF toolset. In: Bernardo, M., Corradini, F. (eds.) Proc. Formal Methods for the Design of Real-Time Systems (SFM-RT 2004), vol. 3185 of Lecture Notes in Computer Science, pp. 237\u2013267. Springer (2004)","DOI":"10.1007\/978-3-540-30080-9_8"},{"key":"9001_CR7","doi-asserted-by":"crossref","unstructured":"Bruni, R., Meseguer, J.: Generalized rewrite theories. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) Proc. 30th International Colloquium on Automata, Languages and Programming (ICALP 2003), vol. 2719 of Lecture Notes in Computer Science, pp. 252\u2013266. Springer (2003)","DOI":"10.1007\/3-540-45061-0_22"},{"key":"9001_CR8","unstructured":"Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)"},{"key":"9001_CR9","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theor. Comput. Sci. 285, 187\u2013243 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"9001_CR10","unstructured":"Clavel, M., D\u00faran, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.1.1), April 2005. http:\/\/maude.cs.uiuc.edu"},{"key":"9001_CR11","unstructured":"Clavel, M., Meseguer, J.: Axiomatizing reflective logics and languages. In: Kiczales, G. (ed.) Reflection\u201996, pp. 263\u2013288 (1996). http:\/\/jerry.cs.uiuc.edu\/reflection\/"},{"key":"9001_CR12","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/S0304-3975(01)00360-7","volume":"2852","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Meseguer, J.: Reflection in conditional rewriting logic. Theor. Comput. Sci. 285(2), 245\u2013288 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"9001_CR13","doi-asserted-by":"crossref","unstructured":"Ding, H., Zheng, C., Agha, G., Sha, L.: Automated verification of the dependability of object-oriented real-time systems. In: Proc. 9th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems (WORDS\u201903). IEEE Computer Society Press (2003)","DOI":"10.1109\/WORDS.2003.1267505"},{"key":"9001_CR14","doi-asserted-by":"crossref","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Fourth International Workshop on Rewriting Logic and its Applications, vol. 71 of Electronic Notes in Theoretical Computer Science. Elsevier (2002)","DOI":"10.1016\/S1571-0661(05)82534-4"},{"key":"9001_CR15","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. Softw. Tools Technol. Trans. 1, 110\u2013122 (1997)","journal-title":"Softw. Tools Technol. Trans."},{"key":"9001_CR16","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57, 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"9001_CR17","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"235","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9001_CR18","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1109\/65.819171","volume":"141","author":"S. Kasera","year":"2000","unstructured":"Kasera, S., Bhattacharyya, S., Keaton, M., Kiwior, D., Kurose, J., Towsley, D., Zabele, S.: Scalable fair reliable multicast using active services. IEEE Netw. Mag. (Special Issue on Multicast) 14(1), 48\u201357 (2000)","journal-title":"IEEE Netw. Mag. (Special Issue on Multicast)"},{"key":"9001_CR19","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transfer 1(1\u20132), 134\u2013152 (1997)","DOI":"10.1007\/s100090050010"},{"key":"9001_CR20","unstructured":"Lien, E.: Formal modelling and analysis of the NORM multicast protocol using Real-Time Maude. Master\u2019s thesis, Department of Linguistics, University of Oslo, 2004."},{"key":"9001_CR21","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1007\/BF01191722","volume":"30","author":"Z. Manna","year":"1993","unstructured":"Manna, Z., Pnueli, A.: Models for reactivity. Acta Informatica 30, 609\u2013678 (1993)","journal-title":"Acta Informatica"},{"key":"9001_CR22","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) Proc. WADT\u201997, vol. 1376 of Lecture Notes in Computer Science, pp. 18\u201361. Springer (1998)","DOI":"10.1007\/3-540-64299-4_26"},{"key":"9001_CR23","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Caccamo, M.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In Baresi, L., Heckel, R. (eds.) Fundamental Approaches to Software Engineering (FASE\u201906), vol. 3922 of Lecture Notes in Computer Science, pp. 357\u2013372. Springer (2006).","DOI":"10.1007\/11693017_26"},{"key":"9001_CR24","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Keaton, M., Meseguer, J., Talcott, C., Zabele, S.: Specification and analysis of the AER\/NCA active network protocol suite in Real-Time Maude. In: Hussmann, H. (ed.) Fundamental Approaches to Software Engineering (FASE 2001), vol. 2029 of Lecture Notes in Computer Science, pp. 333\u2013347. Springer (2001)","DOI":"10.1007\/3-540-45314-8_24"},{"key":"9001_CR25","unstructured":"\u00d6lveczky, P.C., Meseguer, J., Talcott, C.L.: Specification and analysis of the AER\/NCA active network protocol suite in Real-Time Maude. Technical Report UIUCDCS-R-2004-2467, Department of Computer Science, University of Illinois at Urbana-Champaign (2004) Available at http:\/\/www.ifi.uio.no\/RealTimeMaude"},{"key":"9001_CR26","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Real-Time Maude: A tool for simulating and analyzing real-time and hybrid systems. In Futatsugi, K. (ed.) Third International Workshop on Rewriting Logic and its Applications, vol. 36 of Electronic Notes in Theoretical Computer Science. Elsevier (2000) http:\/\/www.elsevier.nl\/locate\/entcs\/volume36.html","DOI":"10.1016\/S1571-0661(05)80134-3"},{"key":"9001_CR27","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1016\/S0304-3975(01)00363-2","volume":"285","author":"P.C. \u00d6lveczky","year":"2002","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theor. Comput. Sci. 285, 359\u2013405 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"9001_CR28","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Thorvaldsen, S.: Formal modeling and analysis of wireless sensor network algorithms in Real-Time Maude. In 20th International Parallel and Distributed Processing Symposium (IPDPS 2006). IEEE Computer Society Press (2006)","DOI":"10.1109\/IPDPS.2006.1639414"},{"key":"9001_CR29","unstructured":"\u00d6lveczky, P.C.: Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic. PhD thesis, University of Bergen (2000) Available at http:\/\/maude.cs.uiuc.edu\/papers"},{"key":"9001_CR30","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude 2.1 Manual (2004) http:\/\/www.ifi.uio.no\/RealTime Maude\/","DOI":"10.1016\/j.entcs.2004.06.015"},{"key":"9001_CR31","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P. Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theor. Comput. Sci. 285, 487\u2013517 (2002)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"9001_CR32","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: Kronos: A verification tool for real-time systems. Softw. Tools Technol. Trans. 1(1\u20132), 123\u2013133 (1997)","journal-title":"Softw. Tools Technol. Trans."}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9001-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-007-9001-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9001-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,10]],"date-time":"2023-05-10T19:41:36Z","timestamp":1683747696000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-007-9001-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2,24]]},"references-count":32,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2007,4,4]]}},"alternative-id":["9001"],"URL":"https:\/\/doi.org\/10.1007\/s10990-007-9001-5","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2,24]]}}}