Angelo Garganti and Angelo Morzenti: TRIO Specification
of a Steam Boiler Controller
We specify a controller for a steam boiler starting from an informal
descriptions of its requirements. The specification is formalized in the
temporal logic TRIO and its object-oriented extension TRIO+. To obtain a
maximum of abstraction and reuse we make the specification parametric with
respect to all equipment and hardware features, and we avoid to impose any
particular strategy in the management of the available resources and in the
control of the critical physical quantities. We illustrate how the
specification can be validated by means of abstract interpretation, how it
can be used to derive test cases for verification, and we discuss how its
modular, object-oriented structure can drive the design and implementation
in software of the specified apparatus.