Back to Case studies list...

Automated Highway Control

We consider a highway section, with the aim to control vehicles and avoid collisions. A small part of such a section is depicted in Fig. 5. This section is modeled as a discrete system that consists of a set of vehicles, moving on n lanes of length L, numbered from 0 to n-1. Moves of a vehicle include driving forward and changing lanes. Vehicles exiting the range of the section are deleted from the set. Crashes are detected by estimating overlaps of danger zones (shadowed rectangles in the figure), which are computed based on current vehicle speed and physical constraints.


Fig. 5. A highway section.

Modeling the Highway System with VeriJ

To analyze this system, we first build a set of VeriJ classes, represented in Fig. 6:
  1.  a Vehicle has a forward and lateral speed (noted xspeed and yspeed) as well as coordinates with respect to these two axes. It also has a boolean property “isControlled”that indicates whether the vehicle is currently controlled.
  2. The VehicleList is a holder for a list of Vehicles, that supports global operations on the list (reordering. . . ).
  3. The Delays class represents for each lane the current time before a new vehicle can be inserted on that lane (at left-most position).
  4. The Highway class represents the full system and contains the scaling parameters of the model and the main actions.
  5. The TestHighway class instantiates the Highway class and contains the engine of the system.
  6. Constants like number of lanes, maximum and minimum xspeed, etc. are contained in a class Constants.


Fig. 6. Class diagram for highway system.
We then define the behavior of the objects in the code follows, as operations of their corresponding VeriJ classes.


VeriJ Source code