Concurrent Programming (19530-V)

Achtung: Beachtet bitte, dass dieses Übungsblatt wieder zu Donnerstag bearbeitet werden soll. Die Lösung zu Übung 9 wird am 25.1.2002 auf die Kurs-Website gestellt, damit ihr sie für diese Übung benutzen könnt. Dies ist das letzte Übungsblatt des Kurses.

1. Aufgabe

Definiert für die Lösung der Übung 9 eine progress property, die aussagt, dass mindestens ein Roboter sich in mindestens eine Richtung unendlich oft bewegen kann. Benutzt LTSA um das Modell zu analysieren. Findet ihr irgendwelche Verletzungen der progress property ("progress violations")? Wenn ja, beschreibt das Szenario, in dem die Verletzung auftritt, und wie man das Problem beseitigen könnte.

2. Aufgabe

Definiert für die Lösung der Übung 9 eine safety property, die aussagt, dass ein einzelnes Feld niemals doppelt belegt wird. Benutzt LTSA um das Modell zu analysieren. Findet ihr irgendwelche Verletzungen der safety property ("safety violations")? Wenn ja, beschreibt das Szenario, in dem die Verletzung auftritt, und wie man das Problem beseitigen könnte.

Hinweis: Das Formulieren der safety property ist etwas schwieriger als das der progress property. Seht euch die Folien der Vorlesung über Model-based Design nochmal an, wo wir diskutierten, wie man safety properties in Modellen miteinander komponiert. Ihr werdet das Modell wahrscheinlich etwas verändern müssen.