Download Chapter 12 THE ADAPTIVE CRUISE CONTROLLER CASE STUDY

12. The Adaptive Cruise Controller Case Study
3
representation from a different perspective was achieved. We discovered no
disadvantages of combining these Booleans although we did not attempt a
refinement. This representation generated a collation of related operations
that all transitions the system between its main operational conditions such
as cruiseBecomesNotAllowed, cruiseOff etc.
Similarly, a variable representing the state of the closest obstacle was
identified resulting in a collation of operations related to the obstacle status.
We decided on a natural segregation of the model into two classes as given
in Figure 1.
CRUISE
VehicleTryKeepSpeed : BOOL = FALSE
VehicleTryKeepTimeGap : BOOL = FALSE
TimeGapAttitudeWouldBeMore : BOOL = FALSE
SetCruiseSpeed(vtks : BOOL, vtktg : BOOL, tgawbm : BOOL)
CruiseBecomesNotAllowed()
CruiseOff()
CruiseActivationDelayFinished()
CruiseActivationFinished(vtks : BOOL, vtktg : BOOL)
CruiseMightBecomeAllowed()
VehicleManageObstacle(vtks : BOOL, vtktg : BOOL)
VehicleTransientChanges(vtks : BOOL, vtktg : BOOL)
KeepingTGBecomesDisallowed(vtks : BOOL, vtktg : BOOL)
KeepingTGBecomesAllowed(vtks : BOOL, vtktg : BOOL)
VehicleReactionDelay()
1 +cruise
<<constant>>
1 +closestObstacle
OBSTACLE
changed : BOOL = FALSE
ObstacleNewClose()
ObstacleNewFar()
ObstacleDistanceBecomesBig()
ObstacleDisappears()
ObstacleDistanceBecomesClose(vtks : BOOL, vtktg : BOOL, tgawbm : BOOL)
Figure 1: Class Diagram for the Cruise Controller
The classes are CRUISE and OBSTACLE. Note, that the case study, just
has a single instance of each class. This enabled the use of an association to
represent closestObstacle (since associations are links between instances),
which either is an unnecessary complication compared to the original B
model, or is necessary to create valid invariants for UML-B model. For each
class, the behaviour is defined as a state diagram. Figure 2 gives the state
diagram from class OBSTACLE and Figure 3 shows the corresponding B
code with invariants.