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.