School of Computing

Consistency and refinement for partial specification in Z

E. Boiten, J. Derrick, H. Bowman, and M. Steen

In M.-C. Gaudel and J. Woodcock, editors, FME'96: Industrial Benefit of Formal Methods, Third International Symposium of Formal Methods Europe, volume 1051 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, March 1996.

Abstract

This paper discusses theoretical background for the use of Z as a language for partial specification, in particular techniques for checking consistency between viewpoint specifications. The main technique used is unification, i.e. finding a (candidate) least common refinement. The corresponding notion of consistency between specifications turns out to be different from the known notions of consistency for single Z specifications. A key role is played by correspondence relations between the data types used in the various viewpoints.

Note: extended version available as Constructive consistency checking for partial specification in Z.

Download publication 57 kbytes

Bibtex Record

@conference{192,
author = {E. Boiten and J. Derrick and H. Bowman and M. Steen},
title = {Consistency and refinement for partial specification in {Z}},
month = {March},
year = {1996},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1996/192},
    ISBN = {3-540-60973-3},
    booktitle = {FME'96: Industrial Benefit of Formal Methods, Third             International Symposium of Formal Methods Europe},
    editor = {M.-C. Gaudel and J. Woodcock},
    publisher = {Springer-Verlag},
    refereed = {yes},
    series = {Lecture Notes in Computer Science},
    volume = {1051},
}

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

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

Last Updated: 21/03/2014