The Simulator


The goal of this case study was to get acquainted with the use of formal methods for the specification of reactive systems and with the application domain. The experience gained should be distributed within the Sonderforschungsbereich.


This case study is performed by the members of team 1, representing all subprojects of the Sonderforschungsbereich 501.

The application domain, within which the case study is performed, is building automation systems.

Work done

The actual task was to describe formally an event-driven simulator for heat flow within a building. Thereby opening and closing of windows and doors and the weather conditions had to be considered. It had to be possible to maintain a strict binding of simulation and real time or to run the simulation faster than real time by a constant factor.

Starting from an informal problem description given by a customer (represented by the head of subproject D1), a requirements specification and a functional design of the system were derived. This was done following the book of Braek and Haugen: Engineering Real Time Systems, Prentice Hall, 1993. An object oriented notation, Message Sequence Charts (MSC), and Specification and Description Language (SDL) were used to produce this documents. Two essential parts (kernel and interface) of the simulator had been identified and the methodology was applied to them separately.

The following documents are available (in english, gzipped Postscript):

Further Work

This work has been continued by actually implementing a (slightly different) simulator within subproject D1, and by repeating this case study within subproject C1.

For further information about the work of team1, look at its homepage.