The goal of this paper is the correct derivation of an implementation of a steam boiler control system. Using a mixed formalism that is presented in [Hoo94b] in which programs and assertional specifications are combined within a unified framework, we refine its top-level specification in a top-down manner. Having the formalism defined in the PVS specification language, the interactive proof checker of PVS is used to check the correctness of each refinement step, therby guarateeing the correctness of the resulting program.

• RT_part.ps