Specification of real-time and hybrid systems in rewriting logic

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 [3], hybrid automata [2], timed and phase transition systems [25], and timed extensions of Petri nets [1,34], 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 [39]. The relationships with the timed rewriting logic approach of Kosiuczenko and Wirsing [22] are also studied. Key words: Rewriting logic; Maude; Executable formal specification; Rea...

• Type: Journal
• Year: 2002
• Where: TCS
• Authors: Peter Csaba Ölveczky, José Meseguer
• Keywords: Hybrid Systems, Real-time, Systems, TCS 2002, Theoretical Computer Science