## Verifying Abstractions of Timed Systems

*Serdar Tasiran, Rajeev Alur, Robert P. Kurshan, and
Robert K. Brayton*
Given two descriptions of a real-time system
at different levels of abstraction,
we consider the problem of proving that the
refined representation is a correct implementation of the abstract
one.
To avoid the complexity of building a representation for
the refined system in its entirety, we develop a compositional framework
for the implementation check to be carried out in a module-by-module
manner using assume-guarantee proof rules.
On the algorithmic side,
we show that the problem of checking for
timed simulation relations, a sufficient condition for
correct implementation, is decidable.
We study state homomorphisms
as a way of specifying a correspondence
between two modules. We present an algorithm for checking if a
given mapping is a homomorphism preserving timed behaviors.
We have implemented this check in the verifier {\sc Cospan}, and
applied our method to the compositional verification of an asynchronous
queue circuit.

*Proceedings of the Seventh International Conference on Concurrency Theory* (CONCUR 1996), LNCS 1119.