G. Ciobanu, D. Lucanu

Hidden algebra is used to specify object systems, and CCS is used to describe synchronous concurrent systems. We introduce a new specification formalism which we call hidden CCS, formed by extending the object specification with synchronization elements related to the invocation of complementary methods in different object components, and using a CCS coordinating module able to describe the interaction patterns of method invocations.

Various results refer to strong bisimulation over the hidden CCS configurations. We show that weak bisimulation allows for specification development by stepwise refinement. We investigate how the existing tools CWB, BOBJ, Maude can be integrated to describe and verify useful properties of the synchronized concurrent objects.

The hidden CCS specifications can be described in the rewriting logic of Maude. Finally we present the first steps towards a new CTL verification tool for hidden CCS.

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

Full Document (PS)

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",
    url = 	"https://publications.info.uaic.ro/technical-reports/archive/tr03-05-2003-specification-and-verification-of-synchronized-concurrent-objects/"
}