Der Simulator

Ziel

Das Ziel dieser Fallstudie war es, sich mit der Anwendung formaler Methoden bei der Erstellung von Spezifikationen reaktiver Systeme und mit der Anwendungsdomäne vertraut zu machen. Die gewonnene Erfahrung sollte im SFB gestreut werden.

Kontext

Die Fallstudie wurde von den Mitgliedern von Team 1 durchgeführt, welche die Projekte des Sonderforschungsbereichs 501 repräsentieren.

Die Anwendungsdomäne für diese Fallstudie ist die Gebäudeautomation.

Geleistete Arbeit

Die Aufgabe war die Spezifikation eines ereignisgesteuerten Simulators für den Wärmefluß in einem Gebäude. Dazu war es notwendig, das Öffnen und Schließen von Fenstern und Türen zu berücksichtigen. Es sollte möglich sein, eine enge Bindung zwischen realer und simulierter Zeit aufrechtzuerhalten, sowie die Simulation um einen konstanten Faktor schneller als die reale Zeit ablaufen zu lassen.

Ausgehend von einer informellen Problembeschreibung des Kunden (diese Rolle wurde vom Leiter des Projekts D1 übernommen), wurden eine Anforderungsspezifikation und ein funktionales Design des Systems entwickelt. Dabei wurde das Buch von Braek und Haugen Engineering Real Time Systems, Prentice Hall, 1993 zugrundegelegt. Eine objektorientierte Notation, Message Sequence Charts (MSC), und die Specification and Description Language (SDL) wurden zur Erstellung dieser Dokumente verwendet. Zwei Subsysteme (Simulatorkern und -Interface) wurden isoliert, und die Methodologie wurde auf beide nochmals angewendet.

Folgende Dokumente sind verfügbar (in Englisch, gzipped Postscript):

Ergänzende Arbeiten

Im Projekt C1 wurde diese Fallstudie wiederholt. Im Projekt D1 wurde ein (leicht modifizierter) Simulator implementiert.

Weitere Informationen zur Arbeit von Team 1 finden sich auf der Homepage.


Navigation


deiss@informatik.uni-kl.de