Towards a Z method: the Two Button Press case study

Author

Hall, J.G. ; Jacob, J.L. ; McDermid, John A. ; Toyn, I.

Author_Institution

Dept. of Comput. Sci., York Univ., UK

fYear

1995

fDate

34838

Firstpage

42491

Lastpage

42493

Abstract

The Two Button Press case study demonstrates the formal specification and refinement of a simple safety critical system. The work is experimental in nature, and does not yet represent a `production quality´ development method. We present a summary of the stages of the formal development. We then draw a number of conclusions about the application of formal methods to parts of the development process, and their combination for full coverage. The specification method used in the case study combines Statecharts, Z and the SPARK subset of Ada for the description and analysis of the discrete controller subsystem, and a prototype notation, Extended Real Time Logic, for the analysis of the relationship of some aspects of discrete and continuous systems. The combined approach is fairly novel, but relatively straight-forward, at least for the functional properties of the system. Tool support has allowed the detailed examination of certain parts of the development, including the refinement of the Z specification to SPARK code

Keywords

Ada; formal logic; formal specification; real-time systems; safety-critical software; software tools; specification languages; Ada SPARK subset; SPARK code; Statecharts; Two Button Press case study; Z specification refinement; continuous systems; discrete controller subsystem; discrete systems; extended real time logic; formal development; formal specification; functional properties; safety critical system; tool support;

fLanguage

English

Publisher

iet

Conference_Titel

Practical Application of Formal Methods, IEE Colloquium on

Conference_Location

London

Type

conf

DOI

10.1049/ic:19950708

Filename

477887