| ## 13 Case Study: The Steam-Boiler Control System Michel Bidoit1 and Peter D. Mosses2 1 Laboratoire Spécification et Vérification, CNRS UMR 8643 École Normale Supérieure de Cachan 61, Avenue du Président Wilson, 94235 Cachan Cedex, France `bidoit@lsv.ens-cachan.fr` 2 University of Aarhus, BRICS and Department of Computer Science Aabogade 34, 8200 Aarhus N, Denmark `pdmosses@brics.dk` 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.1 1 This chapter partially relies on an earlier work published in [8] where the PLUSS specification language [7,9] was used together with the Larch prover [25]. However, the specification methodology illustrated in this chapter is significantly improved, and moreover CASL provides several features that lead to a much more concise and perspicuous specification, as illustrated later in this chapter. LNCS 2900, pp. 155 - 190 Full article in PDF lncs@springer.de © Springer-Verlag Berlin Heidelberg 2004