Towards a Z method: the Two Button Press case study

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