School of Computing

Separating component and context specification using promotion

John Derrick and Eerke Boiten

In K. Araki, A. Galloway, and K. Taguchi, editors, International conference on Integrated Formal Methods 1999 (IFM'99), pages 182-196. Springer, July 1999.

Abstract

In this paper we discuss how the specification of components may be separated from the description of the context in which they are used. There are a number of ways in which this might be possible and here we show how to use the technique of promotion in Object-Z to combine components which are specified using process algebras.

We discuss two approaches, the first is to separate out the specification into two distinct viewpoints written in different languages. These viewpoints are then combined by a process of translation and unification. The second approach will be to use hybrid languages composed of a combination of CSP and Object-Z. We also consider how to refine such component based descriptions and consider issues of compositionality.

Download publication 198 kbytes (PostScript)

Bibtex Record

@inproceedings{816,
author = {John Derrick and Eerke Boiten},
title = {Separating component and context specification using Promotion},
month = {July},
year = {1999},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1999/816},
    ISBN = {18523310710},
    booktitle = {International conference on Integrated Formal Methods 1999 (IFM'99)},
    editor = {K. Araki and A. Galloway and K. Taguchi},
    publisher = {Springer},
    refereed = {yes},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014