Timed rewriting logic with an application to object-based specification

AbstractIn this paper timed rewriting logic is presented and its application to the specification of real-time object-oriented systems is shown by an example.Time rewriting logic (TRL) is an extension of Meseguer's rewriting logic. The functional and the static properties of a system are described by algebraic specifications, whereas the behaviour of a process is described by nondeterministic term rewriting where each rewriting step is labelled by a time stamp or a time interval.Thus our approach is similar to timed transition systems and can be seen as a generalization of timed automata combined with algebraic specifications. The approach is illustrated by several examples, such as clocks, time out and timer.As the main application we present Timed Maude, an object-based specification language for real-time concurrent systems. Timed Maude is a timed variant of Meseguer's language Maude which is based on rewriting logic. The algebraic specification part and the module part of Maude are kept unchanged in Timed Maude, only concurrent rewriting is replaced by TRL