Cruise Control Example

This is a Java 1.1 simulation of a simple automobile cruise control. We used it as a simple example to develop methods to automatically generate tests from formal specifications. A cruise control module lets a driver accelerate to some speed, activate the cruise control, and the module maintains the speed. Getting the module right is not easy. For instance, if the driver steps on the brake, the module should suspend control until the driver indicates it should resume.

The output or state of the module is shown by the 4 lights on the far right. The controls are: ignition, engine run, cruise control selector, brake pedal, and gas pedal. Click on the cruise control setting you want. The other controls toggle when clicked. By the way, the car does not run until the ignition and the engine RUN are on.

The original specification was in SCR, show below in Table 1, which also has a textual representation. We began with an SMV style specification generated from it by Dr. Atlee.

Credits

This example is from a paper by J. M. Atlee and M. A. Buckley, entitled A logic-model semantics for SCR software requirements in Proceedings of the 1996 Internationall Symposium on Software Testing and Analysis, pages 280-292.

The gas and brake pedal are adapted from the picture of the Dead Pedal 3788 courtesy of Lynx Racing. The speedometer is adapted from spedmtr1.gif courtesy of Top Line Web Design.

Created Wed Mar 19 16:32:36 1998