Implementation of a model lift control system from a formal specification

This paper presents one example of the realisation of a real-time implementation from a formal specification. The specification of a lift control system is used to demonstrate the natural mapping between a formal notation and a pragmatic one as supported by a particular integrated project support environment (IPSE). The problem required a real-time implementation for a model lift system using an IPSE called Perspective produced by Systems Designers (Ref. 1). The specification was written in the Calculus of Communicating Systems (CCS) (Ref. 2) and is a simplified description of such a system. It was chosen as the basis for the development because it provided a succinct, precise definition of the requisite functionality. There were other specifications available at the inception of the project, but these were not felt to provide such a suitable basis for the implementation as they were either verbose, less precise or incomplete in their characterisation of the problem. The following sections describe the stages involved in producing the implementation. They outline the problem itself, the specification produced by Jim Woodcock of the Programming Research Group at Oxford University, the IPSE used to implement the solution, and finally the design and an outline of the implementation itself. The section including the specification gives a minimal explanation of CCS. The full version of the specification as presented at the Ada t (UK) Formal Methods Group in November 1984 is included in an appendix together with outline proofs of some important properties of the specification. It is recommended that readers unfamiliar with CCS either read the appendix instead of Section 3, or read (the prose in) Section 3 to try to gain an understanding of the specification without trying to assimilate all the details of the specification. A number of conclusions are drawn in a final section relating to the primary author's experience while undertaking this project.