TR03-03 (2003) – Behavioral Bisimulation and CTL Models for Hidden Algebraic Specifications

D. Lucanu, G. Ciobanu

We use hidden algebra as a formal framework for objectoriented paradigm. We introduce a labeled transition system for eachobject specification model, and then define a suitable notion ofbisimulation 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 asoftware tool allowing SMV model checking.

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

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",
  note = "URL:http://www.infoiasi.ro/~tr/tr.pl.cgi"
}