Model Checking Object-Z Specification Using SPIN

Nowadays, model checking is recognized as an efficient technology for verifying system properties. There are many tools such as SPIN and NuSMV supports model checking that will greatly enhance software systems applicability. However, it is difficult to establish a tool to directly verify Object-Z, because of its high-level abstraction. This paper puts the Object-Z specification into label transition system (LTS), and then translates the LTS into the input language Promela of Spin. Subsequently, the history invariant in Object-Z is described by Linear Temporal Logic (LTL). So the correctness of Object-Z specification can be verified