13 Case Study: The Steam-Boiler Control System

Abstract

In this chapter we illustrate the use of Casl on a fairly large and complex case study, the steam-boiler control system. This case study is particularly interesting since it has been used several times as a competition problem, and many other specification frameworks have been illustrated with it, see [1]. Here we describe how to derive a Casl specification of the steam-boiler control system, starting from the informal requirements provided to the participants of the Dagstuhl meeting Methods for Semantics and Specification, organized jointly by Jean-Raymond Abrial, Egon Börger and Hans Langmaack in June 1995. The aim of this formalization process is to analyze the informal requirements, to detect inconsistencies and loose ends, and to translate the requirements into a Casl specification. During this process we have to provide interpretations for the unclear or missing parts. We explain how we can keep track of these additional interpretations by localizing very precisely in the formal specification where they lead to specific axioms, thereby taking care of the traceability issues. We also explain how the Casl specification is obtained in a stepwise way by successive analysis of various parts of the problem description. Finally we discuss the validation of the Casl requirements specification resulting from the formalization process, and in a last step we refine the requirements specification in a sequence of architectural specifications that describe the intended architecture of the steam-boiler control system.