In this paper Timed Rewriting Logic and its extension Timed Rewriting Logic with Delays are presented.Timed Rewriting Logic is an extension of Meseguer’s Rewriting Logic. The dynamic behaviour of a time dependent system is described by nondeterministic term rewriting where each rewriting step is labeled by a time stamp. The functional and the static properties of a system are described by algebraic specifications. Deduction rules for timed behaviour and a model class semantics are given. The existence of initial models and the decidability of ground finite timed rewriting systems is proven.Timed Rewriting Logic with Delays is used for modeling imprecise real-time constraints. Here the labels of the rewrite steps are time intervals instead of time stamps. The deduction rules and the model class semantics are generalizations of the corresponding notions for Timed Rewriting Logic. The results concerning existence of initial models and decidability of Timed Rewriting Logic specifications are extended to Timed Rewriting Logic with Delays.The approach is illustrated by several examples, such as clocks, time out, timer, and an imprecise oscillator. As the main application we show how Timed Rewriting Logic with Delays can be used to specify clocks with a drift, clocks in a distributed system and Timed Automata.
Weitere Kapitel dieses Buchs durch Wischen aufrufen
- Timed Rewriting Logic for the Specification of Time-Sensitive Systems
- Springer Berlin Heidelberg