A unified linear-time temporal logic solution to the steam-boiler control specification problem

The TLL XYZ/E is a formal language able to represent the dynamic semantics and the static semantics in a unified framework. It supports the whole proc ess of program development, i.e. from the abstract specification to the eff iciently executable program in a formal, precise and convenient way. The st eam boiler control specification problem, a large case study in the fields of real time, hybrid and communication systems, is discussed with XYZ/E. Th e approach covers physical model construction, formal specification, stepwi se refinement, verification, executable program and visual user interface p rogramming.