An Exercise in Conditional Refinement

Abstract

This paper is an attempt to demonstrate the potential of conditional refinement in step-wise system development. In particular, we emphasise the ease with which conditional refinement allows boundedness constraints to be introduced in a specification based on unbounded resources. For example, a specification based on purely asynchronous communication can be conditionally refined into a specification using time-synchronous communication

The presentation is built around a small case-study: A step-wise design of a timed FIFO queue that is partly to be implemented in hardware and partly to be implemented in software. We first specify the external behaviour of the queue ignoring timing and synchronisation. This overall specification is then restated in a time-synchronous setting and thereafter refined into a composite specification consisting of three sub-specifications: A specification of a time-synchronous hardware queue, a specification of an asynchronous software queue, and a specification of an interface component managing the communication between the first two. We argue that the three overall specifications can be related by conditional refinement. By further steps of conditional refinement additional boundedness constraints are introduced. We explain how each step of conditional refinement can be formally verified in a compositional manner