×

zbMATH — the first resource for mathematics

Specification of real-time and hybrid systems in rewriting logic. (English) Zbl 1001.68061
Summary: This paper explores the application of rewriting logic to the executable formal modeling of real-time and hybrid systems. We give general techniques by which such systems can be specified as ordinary rewrite theories, and show that a wide range of real-time and hybrid system models, including object-oriented systems, timed automata, hybrid automata, timed and phase transition systems, and timed extensions of Petri nets, can indeed be expressed in rewriting logic quite naturally and directly. Since rewriting logic is executable and is supported by several language implementations, our approach complements property-oriented methods and tools less well suited for execution purposes, and can be used as the basis for symbolic simulation and formal analysis of real-time and hybrid systems. The relationships with the timed rewriting logic approach of Kosiuczenko and Wirsing are also studied.

MSC:
68Q42 Grammars and rewriting systems
68T27 Logic in artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] van der Aalst, W.M.P., Interval timed coloured Petri nets and their analysis, (), 453-472 · Zbl 0753.68077
[2] 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, Theoret. comput. sci., 138, 3-34, (1995) · Zbl 0874.68206
[3] Alur, R.; Dill, D.L., A theory of timed automata, Theoret. comput. sci., 126, 2, 183-235, (1994) · Zbl 0803.68071
[4] Barr, M.; Wells, C., Category theory for computing science, (1999), Centre de Recherches Mathématiques Montreal
[5] Beeson, M.J., Foundations of constructive mathematics, (1985), Springer Berlin · Zbl 0565.03028
[6] Bergstra, J.A.; Tucker, J.V., Algebraic specification of computable and semicomputable data types, Theoret. comput. sci., 50, 137-181, (1987) · Zbl 0637.68013
[7] Bjørner, N.; Manna, Z.; Sipma, H.B.; Uribe, T.E., Deductive verification of real-time systems using step, (), 22-43 · Zbl 0954.68084
[8] Bornot, S.; Sifakis, J.; Tripakis, S., Modeling urgency in timed systems, (), 103-129
[9] P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau, M. Vittek, ELAN: a logical framework based on computational systems, in: J. Meseguer (Ed.), Proc. First Internat. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, 1996. URL: http://www.elsevier.nl/locate/entcs/volume4.html. · Zbl 0912.68091
[10] M. Clavel, Reflection in general logics and in rewriting logic, with applications to the Maude language, Ph.D. Thesis, University of Navarre, 1998.
[11] M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Martı́-Oliet, J. Meseguer, Metalevel computation in Maude, in: C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Internat. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, Vol. 15, Elsevier, Amsterdam, 1998. URL: http://www.elsevier.nl/locate/entcs/volume15.html. · Zbl 0917.68024
[12] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martı́-Oliet, J. Meseguer, J. Quesada, Maude: Specification and Programming in Rewriting Logic, Computer Science Laboratory, SRI International, Menlo Park, 1999. URL: http://maude.csl.sri.com.
[13] Clavel, M.; Durán, F.; Eker, S.; Meseguer, J.; Stehr, M.-O., Maude as a formal meta-tool, (), 1684-1703
[14] M. Clavel, J. Meseguer, Axiomatizing reflective logics and languages, in: G. Kiczales (Ed.), Proc. Reflection’96, 1996, pp. 263-288. URL: http://jerry.cs.uiuc.edu/reflection/.
[15] M. Clavel, J. Meseguer, Reflection and strategies in rewriting logic, in: J. Meseguer (Ed.), Proc. 1st Internat. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, 1996. URL: http://www.elsevier.nl/locate/entcs/volume4.html. · Zbl 0917.68107
[16] Futatsugi, K.; Diaconescu, R., Cafeobj report, AMAST series, (1998), World Scientific Singapore
[17] Goguen, J.A.; Meseguer, J., Order-sorted algebra iequational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoret. comput. sci., 105, 217-273, (1992) · Zbl 0778.68056
[18] Halbwachs, N.; Caspi, P.; Raymond, P.; Pilaud, D., The synchronous dataflow programming language lustre, Proc. IEEE, 79, 9, 1305-1320, (1991)
[19] Hanisch, H.M., Analysis of place/transition nets with timed arcs and its application to batch process control, (), 282-299
[20] T.A. Henzinger, P.-H. Ho, H. Wong-Toi, HyTech: a model checker for hybrid systems, Software Tools Technol. Transfer 1 (1997) 110-122. See also HyTech home-page at URL: http://www-cad.eecs.berkeley.edu/ tah/HyTech/. · Zbl 1060.68603
[21] S. Kasera, S. Bhattacharyya, M. Keaton, D. Kiwior, J. Kurose, D. Towsley, S. Zabele, Scalable fair reliable multicast using active services, Tech. Report TR 99-44, University of Massachusetts, Amherst, CMPSCI, 1999.
[22] Kosiuczenko, P.; Wirsing, M., Timed rewriting logic with an application to object-based specification, Sci. comput. programming, 28, 2-3, 225-246, (1997) · Zbl 0877.68071
[23] K.G. Larsen, P. Pettersson, W. Yi, U{\scPPAAL} in a nutshell, Software Tools Technol Transfer 1(1,2) (1997) 134-152. See also U{\scPPAAL} home-page at URL: http://www.uppaal.com/. · Zbl 1060.68577
[24] Lynch, N., Distributed algorithms, (1996), Morgan Kaufmann Los Altos, CA · Zbl 0877.68061
[25] Manna, Z.; Pnueli, A., Models for reactivity, Acta inform., 30, 609-678, (1993) · Zbl 0790.68041
[26] Z. Manna, A. Pnueli, Clocked transition systems, in: Proc. Internat. Logic and Software Engineering Workshop, Beijing, August 1995. Also available as Stanford University CSD Tech. Report STAN-CS-TR-96-1566. URL: http://theory.stanford.edu/ zm/new-papers.html.
[27] Manna, Z.; Sipma, H., Deductive verification of hybrid systems using step, (), 305-318
[28] Meseguer, J., General logics, (), 275-329
[29] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoret. comput. sci., 96, 73-155, (1992) · Zbl 0758.68043
[30] Meseguer, J., Rewriting logic as a semantic framework for concurrencya progress report, (), 331-372
[31] Meseguer, J., Membership algebra as a logical framework for equational specification, (), 18-61 · Zbl 0903.08009
[32] Meseguer, J., Research directions in rewriting logic, (), 347-398 · Zbl 0940.68069
[33] Meseguer, J.; Montanari, U., Petri nets are monoids, Inform. and comput., 88, 105-155, (1990) · Zbl 0711.68077
[34] Morasca, S.; Pezzè, M.; Trubian, M., Timed high-level nets, J. real-time systems, 3, 165-189, (1991)
[35] P.C. Ölveczky, Specification and analysis of real-time and hybrid systems in rewriting logic, Ph.D. Thesis, University of Bergen, 2000. Available at URL: http://maude.csl.sri.com/papers.
[36] P.C. Ölveczky, M. Keaton, J. Meseguer, C. Talcott, S. Zabele, Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude, FASE 2001, to appear. Available at URL: http://maude.csl.sri.com/papers, 2001. · Zbl 0977.68865
[37] Ölveczky, P.C.; Kosiuczenko, P.; Wirsing, M., An object-oriented algebraic steam-boiler control specification, (), 379-402
[38] P.C. Ölveczky, J. Meseguer, Specifying real-time systems in rewriting logic, in: J. Meseguer (Ed.), Proc. First Internat. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, 1996. URL: http://www.elsevier.nl/locate/entcs/volume4.html. · Zbl 0912.68098
[39] P.C. Ölveczky, J. Meseguer, Real-Time Maude: a tool for simulating and analyzing real-time and hybrid systems, in: K. Futatsugi (Ed.), Third Internat. Workshop on Rewriting Logic and its Applications, 2000, Electronic Notes in Theoretical Computer Science, Vol. 36, Elsevier, Amsterdam, 2000. · Zbl 0962.68109
[40] Rabin, M., Computable algebrageneral theory and theory of computable fields, Trans. amer. math. soc., 95, 341-360, (1960) · Zbl 0156.01201
[41] Reisig, W., Petri nets, EATCS monographs on theoretical computer science, Vol. 4, (1985), Springer Berlin · Zbl 0521.68057
[42] The Stanford Temporal Prover. URL: http://www-step.stanford.edu/.
[43] L.J. Steggles, P. Kosiuczenko, A timed rewriting logic semantics for SDL: a case study of the alternating bit protocol, in: C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Internat. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, Vol. 15, Elsevier, Amsterdam, 1998. URL: http://www.elsevier.nl/locate/entcs/volume15.html. · Zbl 0917.68116
[44] Stehr, M.-O.; Meseguer, J.; Ölveczky, P.C., Rewriting logic as a unifying framework for Petri nets, (), 250-303 · Zbl 1017.68080
[45] Viry, P., Rewritingan effective model of concurrency, (), 648-660
[46] S. Yovine, Kronos: a verification tool for real-time systems, Software Tools Technol. Transfer 1(1/2) (1997). See also Kronos home-page at URL: http://www-verimag.imag.fr/TEMPORISE/kronos. · Zbl 1060.68606
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.