TY - JOUR
T1 - Specification of real-time and hybrid systems in rewriting logic
AU - Ölveczky, Peter Csaba
AU - Meseguer, José
N1 - Funding Information:
Supported by DARPA through Rome Laboratories Contract F30602-97-C-0312, by DARPA and NASA through Contract NAS2-98073, by ODce of Naval Research Contract N00014-96-C-0114, and by National Science Foundation Grant CCR-9633363. ∗Corresponding author. Tel.: +47-22840125; fax: +47-22852401. E-mail address: peterol@i .uio.no (P.C. Olveczky).( 1Supported by The Norwegian Research Council.
PY - 2002/8/28
Y1 - 2002/8/28
N2 - 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.
AB - 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.
KW - Hybrid systems
KW - Maude
KW - Real-time object-oriented systems
KW - Real-time systems
KW - Rewriting logic
KW - Timed Petri nets
UR - http://www.scopus.com/inward/record.url?scp=0037190149&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0037190149&partnerID=8YFLogxK
U2 - 10.1016/S0304-3975(01)00363-2
DO - 10.1016/S0304-3975(01)00363-2
M3 - Article
AN - SCOPUS:0037190149
SN - 0304-3975
VL - 285
SP - 359
EP - 405
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 2
ER -