Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method
Kazuhiro Ogata, Kokichi Futatsugi · Electronic Notes in Theoretical Computer Science · 2008
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.