The DisCo Home Page

Taxi Cabs

This is a simple example that illustrates the use of DisCo and formal verification of DisCo specifications. Our purpose is to model a system in which cabs and customers can enter taxi stands, where a cab can then pick up a customer. The specification is developed using stepwise refinement.

Stands

The first system introduces taxi stands. Taxi stands have no attributes and hence no associated 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. The specification is:

system stands is
  class taxi_stand is
  end;
end;

Cabs

Cabs can simply enter or exit stands. The specification of cabs is:

system cabs import stands; is
  class cab is
    state *on_the_road, at_stand(where : taxi_stand);
  end;

  action enter_stand
  by cb : cab; s : taxi_stand is
  when cb.on_the_road do
    ->cb.at_stand(s);
  end;

  action exit_stand
  by cb : cab is
  when cb.at_stand do
    ->cb.on_the_road;
  end;
end;

Customers

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. The specification of customers is:

system customers import stands; is
  class customer is
    state *idle, waiting_for_cab, being_served;
    extend waiting_for_cab by
      where : taxi_stand;
    end;
  end;

  action start_waiting
  by c : customer; s : taxi_stand is 
  when c.idle do
    ->c.waiting_for_cab;
    c.waiting_for_cab.where := s;
  end;

  action stop_waiting
  by c : customer is
  when c.waiting_for_cab do
    ->c.idle;
  end;

  action get_service
  by c : customer is
  when c.waiting_for_cab do
    ->c.being_served;
  end;

  action release_service
  by c : customer is
  when c.being_served do
    ->c.idle;
  end;
end;

Final Result

In the final step, the specifications of customers and cabs are combined. In this specification, a ride starts when a cab leaves a stand with a customer, who simultaneously gets service. The specification is:

system rides import cabs, customers; 
combined start_ride of cabs.exit_stand, customers.get_service; is
  extend cab by
    extend on_the_road by
      state *free, engaged;
    end;
  end;

  extend customer by
    state *outside, in_cab;
    extend in_cab by
      which : cab;
    end;
  end;

  refined start_ride is
  when ... cb.at_stand.where = c.waiting_for_cab.where
       and c.outside do
    ...
    ->c.in_cab;
    c.in_cab.which := cb;
    ->cb.on_the_road.engaged;
  end;

  refined end_ride of release_service
  by ... cb : cab is
  when ... c.in_cab.which = cb
       and cb.on_the_road.engaged do
    ->c.outside;
    ->cb.on_the_road.free;
    ...
  end;

  refined get_service is
  when ... false do
    ...
  end;

  refined enter_stand is
  when ... cb.on_the_road.free do
    ...
  end;

end;

Verification

The specification is mapped to two PVS theories: rides, and rides_assertions. The former gives the definitions corresponding to classes and actions in the DisCo specification, and the latter gives the assertions.

We set out to verify two simple invariants, idle_outside and inside_engaged. The first invariant states that whenever a customer is idle, he is also outside a cab:

 assert idle_outside is
    and/ c : customer :: c.idle => c.outside;

This assertion cannot be proved by itself, but requires the following strengthening.

 assert idle_outside_strengthening is
    and/ c : customer :: 
	not(c.waiting_for_cab and not c.outside)
	and not(c.idle and not c.outside)
	;

This assertion is verified straightforwardly using the PVS theorem prover. The situation is similar with the assertion inside_engaged.

  assert inside_engaged is
    and/ c : customer :: and/ cb : cab ::
      c.in_cab.which = cb => cb.on_the_road.engaged;

  assert inside_engaged_strengthening is
    and/ c1 , c2 : customer; cb : cab ::
       not(c1.in_cab.which = cb and not cb.on_the_road.engaged)
       and not(c1.in_cab.which = cb
	       and c2.in_cab.which = cb
	       and c1 /= c2)
     ;

Give feedback.