Refinement through Pictures: Formalising Syntropy Refinement

Concepts

K. Lano, J. Bicarregui

Dept. of Computing, Imperial College, 180 Queens Gate, London, SW7 2BZ

October 31, 1997

Abstract
This paper provides techniques for formally justifying the refinement steps given for the Syntropy method of Cook and Daniels.

It uses a temporal logic formalism, the Object Calculus, to formalise the models of Syntropy in modules which are theories, linked by theory-preserving morphisms. Refinements are also characterised by particular forms of interpretations between theories.

The intention is to provide support for a system which allows refinement steps to be carried out via diagrammatic descriptions, rather than mathematical formulae, and hence to enhance the usability of a formal approach to object-oriented software development.

1 Introduction

Syntropy [4] is a methodology for object-oriented analysis and design similar to OMT [17] with additional formal specification elements derived from Z [19]. It represents a significant advance over previous objectoriented methods in giving mathematical specifications of data models and dynamic behaviour. Concepts from Syntropy have been used in the UML [18], particularly in the development of its object constraint language.

Three distinct levels of modelling are used in Syntropy. At each of these three levels, type view diagrams depict the structure of object classes. Objects have attributes of non-object types. Associations between classes are depicted by connecting lines. Statecharts [9] are also used at each of the three levels. However, different models of communication are used at each level of abstraction.

ffl Essential models describe the problem domain of the application. They describe the system as a whole including the proposed software solution and its environment. They use events and broadcast communications to abstract from the localisation of methods in classes.

ffl Specification models abstractly model the requirements of the software application, hence defining the software/environment boundary. They decompose a reaction to an external event into a series of event generations and internal reactions by specific classes.

ffl implementation models model the required software in detail. In addition, object interaction graphs (termed mechanisms in Syntropy) are used at this level, with object to object message passing.

Syntropy adopts a number of mathematical notations, however, a semantics is only indicated for data models. In addition, there is no formal definition of refinement between models.
There are two main forms of refinement which arise in the Syntropy method:

1. Refinement which involves a change in granularity of the actions of the system, such as factoring a transition which establishes a complex postcondition into a sequence of internal transitions which each establish part of the postcondition.

1st BCS FACS Workshop on Making Object-oriented Methods More Rigorous 1