Case study : The Gas Station
Presentation :
We aim here to study and eventually correct a program with the verification tool Quasar. This program, given below, simulates an automated gas station system consisting of an operator, a pump and a customer.
We easily see that there is a simple and unavoidable deadlock that Quasar reports instantaneously giving us the execution which leads to the deadlock. This one occurs as soon as the customer calls the Finish entry. The pump is then accepting the call and in its turn calling the operator charge entry which is accepted by the operator. Finally the operator calls the customer change entry. Being given the customer hasn't been acknowledged by the pump, we reach a deadlock. Here is the execution corresponding to this one :
Customer -> Operator.Prepay
Operator -> accept Prepay
Operator -> Pump.Activate
Pump -> accept Activate
Customer -> Pump.Start
Pump -> accept Start
Customer -> Pump.Finish
Pump -> accept Finish
Pump -> Operator.Charge
Operator -> Customer.Change
With the execution given by Quasar we easily manage to correct the program. This can be done by removing the Operator.Charge entry call in the pump body from the enclosing accept statement. With this update Quasar reports no deadlock. The verification of more complex properties will soon be available in Quasar but can be done with tools such Prod, a reachability analyzer. For example :
- A client can get gas only if he already payed
- A client who payed always gets his gas
- ...
Major Ada language components added :
- Select statement
Downloads :
Pictures :
|
|
| There is a deadlock in this program | The trace of the sequence leading to the deadlock |
last update : 20/10/2005