A concurrent object-based design notation and its semantics

Cliff Jones

(University of Manchester)

A software development method which makes it possible to verify one set of design decisions before moving to the next stage of design has the potential to save time for developers. For sequential programs, it is not difficult to find formal design methods which are "compositional". But the interference which comes from parallel processes makes compositionality much more elusive. Earlier research on documenting rely and guarantee conditions did something to tame the dragon of interference but the approach still required too much work to expect it to be used even as widely as sequential development methods like VDM. It would appear that constraining the languages in which programs are written is the only way of reducing the work involved. This seminar will exhibit the problem with examples, outline some notations to reason about interference, and explain why concepts from object-oriented programming languages are helpful. Finally, a semantics in terms of the pi-calculus will be sketched.
Tuesday 25th January 1994, 14:30
Seminar Room 322
Department of Computer Science