TR03-05 (2003) – Specification and Verification of Synchronized Concurrent Objects

G. Ciobanu, D. Lucanu

Hidden algebra is used to specify object systems, and CCS is used todescribe synchronous concurrent systems. We introduce a newspecification formalism which we call hiddenCCS, formedby extending the object specification with synchronizationelements related to the invocation of complementary methods in differentobject components, and using a CCS coordinating module able to describethe interaction patterns of method invocations. Various results refer tostrong bisimulation over the hiddenCCS configurations. We show that weakbisimulation allows for specification development by stepwise refinement.We investigate how the existing tools CWB, BOBJ, Maude can be integratedto describe and verify useful properties of the synchronized concurrentobjects. The hiddenCCS specifications can be described in the rewritinglogic of Maude. Finally we present the first steps towards a newCTL verification tool for hiddenCCS.

A concise and revised version of the paper was accepted at the FourthInternational Conference on Integrated Formal Methods(IFM2004).

Bibtex

@TechReport{svsco,
  author = "Gabriel Ciobanu and Dorel Lucanu",
  title = "Specification and Verification of Synchronized Concurrent Objects",
  institution = "``Al.I.Cuza'' University of Ia{c s}i, 
                 Faculty of Computer Science",
  year = "2003",
  number = "TR 03-05",
  note = "URL:http://www.infoiasi.ro/~tr/tr.pl.cgi"
}