Exercises

• 8.1 Each of the rooms in a building has a control station for monitoring and controlling the environment. Each control station measures and displays the current temperature and humidity. For each room, the desired temperature and humidity is set by a pair of dials. If the current readings are outside the desired setting by more than 1%, then the station can control the heating or ventilation accordingly. A central operator station is able to request the current readings from any control station.

• Outline the design structure of a room control station given that it is decomposed into the following processes: sensors, dials, heater – ventilator, display and controller. Provide a model for each process and check that the control station satisfies appropriate safety and progress properties.

• Provide an implementation for the room control station.

• 8.2 A self-service gas station has a number of pumps for delivering gas to customers for their vehicles. Customers are expected to prepay a cashier for their gas. The cashier activates the pump to deliver gas.

• Provide a model for a simple system with two customers and a gas station with one pump and a cashier. Include in the model a range for the different amounts of payment and that a customer is not satisfied (ERROR) if the incorrect amount of gas is delivered:

   range A = 1..3 CUSTOMER = (prepay[a:A]->gas[x:A]->                 if (x==a) then CUSTOMER                           else ERROR            ).

• Check the safety and progress properties for this system.

• Provide a simple Java implementation for the gas station system.

• 8.3 Extend the gas station model in exercise 8.2 to cater for N customers and M pumps. Specify and check a safety property, FIFO, which ensures that customers are served in the order in which they pay.