Research on Model Checking Formal Language Object-Z
WU Cai-yan
Abstract：Object-Z is a high-level abstract language used to represent the specification of the object-oriented system.For lack of support of automatic verification tools,it is difficult to verify the correctness of the specification of the object-oriented system represented by Object-Z.Model checking is such an automatic verification technique.This paper verifies the correctness of the Object-Z specification using model checking tool-SPIN,which translates the Object-Z specification into label transition system (LTS)firstly,and then converts the LTS format into the input language Promelaof SPIN.Subsequently,the history invariant in Object-Z is described by Linear Temporal Logic (LTL).Through verifying the Object-Z specification of the booking system class,the results show that this method is feasible.
Keywords：model checkingObject-ZSPINtemporal logic
Publication Date：2015-01-01
Online Publishing Date：2025-08-15(First online date of this platform, not the publication date of the document)
Pages：7( 29-35 )