Normed simulations

Abstract

In existing simulation proof techniques, a single step in a low-level system may be simulated by an extended execution fragment in a high-level system. As a result, it is undecidable whether a given relation is a simulation, even if tautology checking is decidable for the underlying specification logic. This paper introduces various types of normed simulations. In a normed simulation, each step in a low-level system can be simulated by at most one step in the high level system, for any related pair of states. We show that it is decidable whether a given relation is a normed simulation relation, given that tautology checking is decidable. We also prove that, at the semantic level, normed simulations form a complete proof method for establishing behavior inclusion, provided that the high-level system has finite invisible nondeterminism. As an illustration of our method we discuss the verification in PVS of a leader election algorithm that is used within the IEEE 1394 protocol.