Specification and verification of synchronizing concurrent objects

Abstract

We introduce a new specification formalism which we call hiddenCCS; hidden algebra is used to specify local goals as objects, and CCS is used to describe global goal of the synchronizing concurrent objects. We extend the object specification with synchronization elements associated with methods of different objects, and we use a CCS coordinating module to describe the interaction patterns of methods invocations. Some results refer to strong bisimulation over the hiddenCCS configurations. We investigate how the existing tools BOBJ, CWB, and Maude can be integrated to describe and verify useful properties of the synchronizing concurrent objects. The hiddenCCS specifications can be described in the rewriting logic using Maude. Finally we present the first steps towards temporal specifications and verification for hiddenCCS. © Springer-Verlag 2004.