Towards a formal method for distributed object-oriented systems

Abstract

We present two components of a special purpose formal method intended to support the modelling and development of distributed object-oriented systems. The first component is a language, called Oompa, in which designs for these systems can be expressed. The second is a behavioural specification language called sequential process specifications. Oompa is a strongly-typed class-based object-oriented language. Its objects have private state and support multiple concurrent invocations. The primitive operations of its methods support both object-based and channel based behaviour. We provide two operational semantics for Oompa; a reduction relation, which is intuitive, and a labelled transition system, which is superior for reasoning. We define a type system for Oompa which is statically checkable. We also give thorough consideration to issues of naming in Oompa. Sequential process specifications allow abstract behaviour to be specified and incrementally refined. The language has two binary operators, similar to CSP’s internal and external choice, which assert that a system may or must have certain behaviour. We use sequential process expressions, which form the core of CCS, to describe specific patterns of behaviour and we define what it means for one to satisfy a specification. In terms of this notion of satisfaction, we define a semantics and a refinement relation for the language. Although similar to CSP, we show that our language is semantically different. We demonstrate how our formal method currently supports development by deriving two designs for a concurrent dictionary object.