UPPAAL ist frei verfügbar (akademische Lizenz): http://www.uppaal.org/
Die grundlegenden Elemente von UPPAAL werden in der Vorlesung erklärt. Unten finden Sie eine Reihe von Beispielen als auch Aufgaben die Sie im Labor bearbeiten sollen.
Weitere Hilfestellungen finden Sie hier: http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Allgemein ist UPPAAL "einfach erlernbar" und viele Fragen lassen sich via der Online Hilfe beantworten.
Eine trickreiche Sache ist die Einstellung des "proxies", falls Sie UPPAAL innerhalb der HS KA benutzen wollen. (FYI, UPPAAL benötigt eine Verbindung zu dem Lizenzserver). Hilfestellung zum "proxy" finden Sie hier (siehe Punkt 15): http://www.uppaal.com/index.php?sida=201&rubrik=95
[EDIT:] Auf meinem Mac scheint eine extra Konfiguration wegen proxy aktuell nicht mehr notwendig.
xml das Modell und q die Spezifikation ("queries"), jeweils herunterladen via folgenden links
Lampe xml Modellierung einer Tischlampe mit Helligkeit
SendReceive xml Modellierung von Nachrichtenbasierter Kommunikation
Folgendes Verhalten lässt sich beobachten (via Simulator)
Beachte: Die Aufgabenbeschreibung sagt nichts gegenteiliges aus. Vorteil der formalen Modellierung Wir können dieses Verhalten im Modell genau nachvollziehen (bevor man viel Arbeit in die eigentliche Implementierung steckt)
Aufgabe: Wie könnte man durch eine geeignete Query (TCTL Formel) obigen Ablauf herauskriegen?
Sehr einfach gehalten. Als Erweiterung könnten Sie (eine endliche Anzahl) von Wartestühlen modellieren Beachte: Die Modellierung im Übungsblatt (2-uebung-state-cfa) unterscheidet sich dadurch, dass ein Kunde entweder direkt zum Barbier geht oder zuerst auf einem Stuhl Platz nimmt.
In UPPAAL können wir leider nicht direkt den aktiven Zustand eines Automaten abfragen. Wir führen deshalb (globale) Variablen ein, die den aktuellen Zustand repräsentieren Transitionen bekommen guards (Randbedingungen) die garantieren, dass z.B. der Wolf nicht alleine mit der Ziege auf einer Seite des Ufers bleibt