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.