Concurrent Programming (19530-V)Dr. Richard S. Hall WS 01/02- Übung 7 -Assigned: 11.12.2001Due: 18.12.2001 |
|
1. Exercise a) What is the purpose of a safety property?b) From the lecture on page 7, why does the mutual exclusion safety property fail if the semaphore is initialized to 2? c) How do you create an LTS graph for the process associated with a safety property? d) What is the purpose of a liveness property? 2. Exercise Create an action trace that violates the following safety property: property PS = (a->(b->PS | a->PS) | b->a->b->PS). 3. Exercise An elevator has a maximum capacity of ten people. In the FSP model
of the elevator control system, passengers entering the elevator are signaled
by an enter action and passengers leaving the elevator are signaled by an exit action. Specify a safety property which will check that the system never allows the elevator to have more than 10 occupants when composed with the control process. (You do not need to create the model for the elevator, just assume one exists.) |