language: en

An Assume-Guarantee Rule For Checking Simulation

Thomas A. Henzinger Shaz Qadeer Sriram K. Rajamani and Serdar Tasiran
University of California, Berkeley

The simulation preorder on state transition systems is widely accepted as a useful notion of refinement, both in its own right and as an efficiently checkable sufficient condition for trace containment. For composite systems, due to the exponential explosion of the state space, there is a need for decomposing a simulation check of the form P �s Q, denoting �P is simulated by Q,� into simpler simulation checks on the components of P and Q. We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q, we provide a procedure for constructing a witness relation for P �s Q. We also extend our assume-guarantee rule to account for fairness constraints on transition systems.

Categories and Subject Descriptors: D.2.4 [Software Engineering]: Software/Program Verification� formal methods; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms: Verification Additional Key Words and Phrases: Simulation relations, verification rules

1 Introduction