From Rewrite Theories to Temporal Logic Theories
The work presented here aims at
bridging the gap between executable specifications and formal
verification. In this paper we combine two levels of
description without changing the
framework. The operational level of Maude/rewriting logic and the
property-oriented level of temporal logics are combined. The
combination is done by an embedding. We propose a distributed temporal
logic as an extension of rewriting logic. Rewriting logic is
primarily a logic of change in which the deduction directly
corresponds to the computation. In contrast to that, temporal logic is
a logic to talk about change in a global way. Especially, more
complex system properties such as safety and liveness can be regarded
in a temporal logic setting. In our approach we maintain the
possibility of executing Maude specifications on the rewrite machine
for validation purposes, and add the possibility of formally reasoning
about Maude specifications in a temporal logic setting. The work
presented focuses on object-oriented Maude specifications.