D. Lucanu, G. Ciobanu

We use hidden algebra as a formal framework for object oriented 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 anobject specification. Given two hidden algebra models of an object specification, the bisimilar states satisfy the same set of CTL formulas.

We build a special 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.

A shorter version of the paper was accepted at the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2003).

Full Document (PS)

Bibtex

@TechReport{ctlha,
    author = 	"D. Lucanu and G. Ciobanu",
    title = 	"Behavioral Bisimulation and {C}{T}{L} Models for Hidden Algebraic Specifications",
    institution = "``Al.I.Cuza'' University of Ia{c s}i, Faculty of Computer Science",
    year = 	"2003",
    number = 	"TR 03-03",
    url = 	"https://publications.info.uaic.ro/technical-reports/archive/tr03-03-2003-behavioral-bisimulation-and-ctl-models-for-hidden-algebraic-specifications/"
}