UPPAAL-Modelle als ausführbare Spezifikation in Java

In: Software Engineering 2008 - Workshopband
München (2008), S. 212-218
ISBN: 978-3-88579-216-1
Buchaufsatz / Kapitel / Fach: Informatik
Abstract:
Zustandsautomaten koennen als Modelle umfassend spezifiziert, simuliert und validiert werden. Werden sie im Programmcode umgesetzt, bleibt der formale Bezug zu diesen Modellen jedoch in der Regel nicht vollstaendig erhalten. Dieser Beitrag untersucht, wie Modellentwicklung am Beispiel von UPPAAL und die Umsetzung im Java-Programmcode gleichzeitig geschehen koennen, indem eine Methode zur Spezifikation von Zustandsautomaten im Programmcode skizziert wird. Dieser Programmcode kann sowohl als Zustandsautomat ausgefuehrt, als auch ad hoc in ein UPPAAL-Modell transformiert werden.