|
|
The DisCo Home Page |
       |
A Taxi Cabs SystemThis case study describes the specification of a taxi cab system. The system is a simplified model of a busy Saturday night. Customers wait for taxi cabs at taxi stands, and cabs transfer them from stands to their destinations. We structure the specification in three layers. The layers are:
The top layer introduces a single class. Taxi stands have no attributes, and hence the layer contains no actions. Each stand has, however, a unique identity which can be referred to. The reason this system is needed is that we need to refer to taxi stands in the specifications of cabs and customers, and we want them to refer to the same stands. In DisCo98, the top layer would not be needed. We could introduce separate stands in the separate specifications of cabs and customers, and use multiple inheritance to combine the classes. In the next step, customers and cabs are introduced in independent refinements. Cabs can simply enter or exit stands. A customer can start waiting at a particular stand, and either give up and stop waiting, or get service. Once a customer is being served, he can then release service. In the final step, the specifications of customers and cabs are combined. A ride starts when a cab leaves a stand with a customer, who simultaneously gets service. Give feedback. |