|

Integrated Specification Notations

Research by funded by the Royal Society as a Research Interchange Grant. 

Summary

Complex computer systems are difficult to implement correctly. To aid the process formal methods use mathematics in the specification of a systems requirements and its refinement into more detailed designs and program code. Because complex systems involve many facets (behaviour, communication etc) much recent research has concerned the integration of formal notations in order to use the advantages of each. 

One such approach combines the Object-Z and CSP notations, and in this project we are concerned with techniques for the refinement of specifications written in this style. In particular, we seek to tackle two specific problems in this area: action refinement and the automation of the refinement checking process.

Why and how?

Integrations of formal methods offer the practitioner an approach where different aspects of a system can be specified in the most appropriate notation. Of particular interest are combinations of state-based languages (e.g., Z, Object-Z, B) with process algebras (CSP, CCS, etc), since such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour. A number of proposals exist, each tackling different aspects of the problem, with work on combining Object-Z and CSP having been undertaken by the groups at both Oldenburg and Sheffield/Kent.

The work of Derrick has centred on integrations of Object-Z and CSP that preserve the syntactic and semantic nature of both the languages, and their work is unique in this respect. Papers by Smith and Derrick detail an approach to, not only specification, but also verification and refinement in the combined language.

The work at Oldenburg has centred on a more complex combination, producing a language CSP-OZ, which contains novel features of integration (e.g., involving the use of process definitions within classes). They have done considerable work on mechanising the approach by providing tool-support including preliminary work on model-checking.

In both integrations a common semantic model is used in order to given specifications in the language a well-defined meaning. This common semantic model is based upon the failures-divergences semantics of CSP, and is achieved by deriving the failures-divergences of the Object-Z components via its own semantics.

In addition to specification, both groups have an interest in refinement. The purpose of refinement is to provide a well-defined notion of development where the correctness of a more detailed design can be verified against an abstract specification. Having a common semantic basis for combinations of Object-Z and CSP enables a unified method of refinement to be developed for the integrated notations based upon CSP failures-divergences refinement. This in turn allows state-based simulation methods to be used on the individual components in a specification. The technology has been pushed forward in a number of directions, e.g., by defining simulation rules which allow the structure of the components to be changed in a refinement. However, a number of important open questions remain. These include a means to refine the atomicity of operations and events; a means to mechanise the refinement checking process.

These issues have not been solved in any of the existing integrated notations, and the purpose of this project is to respond to these issues. 

Related projects