Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method

Abstract

The OTS/CafeOBJ method is a formal method to model systems, specify models and verify that models satisfy properties. We propose a way to verify that a state machine S satisfies invariant properties based on a simulation from S to another state machine, which is more abstract than S, in the OTS/CafeOBJ method. Three communication protocols are used as examples to demonstrate the proposed method.