Model Checking for Object Specifications in Hidden Algebra

We use hidden algebra as a formal framework for object paradigm. We introduce a labeled transition system for each object specification model, and then define a suitable notion of bisimulation over these models. The labeled transition systems are used to define CTL models of object specifications. Given two hidden algebra models of an object specification, the bisimilar states satisfy the same set of CTL formulas. We build a canonical CTL model directly from the object specification. Using this CTL model, we can verify the temporal properties using a software tool allowing SMV model checking.