Modular description and verification of concurrent objects

Jean-Paul Bahsoun, Stephan Merz, Corinne Servières

Abstract

The design of large and complex distributed systems requires a modular approach to support reuse and verification. We propose an object-oriented programming model based on concurrently executing communicating agents (concurrent objects) and an associated proof methodology that exploits the class hierarchy to allow for modular verification.

We propose to separate protocol from functionality in class definitions, and advocate separate hierarchies of protocol classes as a way to overcome the inheritance anomaly of concurrent object-oriented programming.

We formalize an agent in Lamport's Temporal Logic of Actions. Modular verification is achieved by restricting inheritance in a way that ensures that subclasses refine superclasses. Interesting properties can thus be verified at an abstract level, ignoring unnecessary implementation detail.

© Springer-Verlag

Available as:  gzip'ed Postscript 

Reference

@InProceedings{bahsoun:modular,
  author =    "Jean Paul Bahsoun and Stephan Merz and
               Corinne Servi\`{e}res",
  title =     "Modular Description and Verification of
               Concurrent Objects",
  series =    "Lecture Notes in Computer Science",
  volume =    1107,
  booktitle = "0bject-Based Parallel and Distributed Computation",
  editor =    "J.-P. Briot and J.-M. Geib and A. Yonezawa",
  year =      1996,
  publisher = "Springer-Verlag",
  address =   "Tokyo, Japan",
  pages =     "168--185"
}