Concurrent Programming (19530-V)Dr. Richard S. Hall WS 01/02- Übung 7 -Assigned: 11.12.2001Due: 18.12.2001 |
|
1. Aufgabe a) Wofür wird eine Sicherheitseigenschaft (safety property) eingesetzt?b) Ausgehend von der Vorlesung (Seite 7): Warum gilt die Sicherheitseigenschaft des gegenseitigen Ausschlusses nicht, wenn die Semaphore mit 2 initialisiert wird? c) Wie erzeugen Sie (evtl. automatisch) einen LTS Graphen für einen Prozess, der eine Sicherheitseigenschaft realisiert? d) Wofür wird eine Lebendigkeitseigenschaft (liveness property) eingesetzt? 2. Aufgabe Generieren Sie eine Spur von Aktionen (event
trace), welche gegen die folgende
Sicherheitseigenschaft verstößt: property PS = (a->(b->PS | a->PS) | b->a->b->PS). 3. Aufgabe Gegeben sei ein Aufzug mit einer maximalen Aufnahmekapazität von 10 Personen. Gehen Sie im folgenden davon aus, dass Ihnen ein FSP Modell vorliegt, welches diesen Aufzug modelliert. Benutzer, die den Aufzug betreten, werden durch eine enter Aktion dargestellt. Für Benutzer, die diesen verlassen, wird die exit Aktion eingesetzt. Spezifizieren Sie eine Sicherheitseigenschaft, die sicherstellt, dass sich maximal 10 Personen gleichzeitig in dem Aufzug befinden. (Hierfür benötigen Sie keine Spezifikation des Verhaltens des Aufzugs.) |