In theory, the approaches to hybrid controller design discussed in the previous section guarantee that the requirements specification is satisfied by design. In practice, system complexity often limits the applicability of automatic controller synthesis methods, and currently, a common approach to the design of hybrid controllers involves independently coming up with a reasonable design for both the discrete and continuous parts. The combined hybrid controller is then put together by means of interfaces, and verification is carried out to ensure that it satisfies certain properties. Typically, some design errors are found, and the verification attempt supplies the design engineer with diagnostic information that is helpful for reformulating the design. The process of simulation, verification attempts, and redesign is iterated until a successful design is obtained.
This approach has been motivated by the success of verification techniques
for finite-state systems. Verification tools for finite state machines have
been in use for years (SPIN [10], SMV [12],
COSPAN [13], VIS) and proven successful for the automatic analysis
of discrete problems such as communication protocols and digital circuits.
The push towards stronger verification techniques has been in the direction
of extending the standard finite state machine results to incorporate
progressively more complicated continuous dynamics. The first extension has
been for systems with clocks [14, 15]. Verification tools
for finite state machines with clocks have been implemented (KRONOS
[16], UPPAAL [17], and Timed COSPAN [28]) and
used successfully for the automatic analysis of real-time hardware, and
software [19].
The possible values of clocks range over the real numbers. Hence the state
space of real-time systems is infinite and automatic verification must
proceed symbolically, by representing sets of states using symbolic
constraints (instead of state enumeration). Symbolic state space analysis
techniques have been extended from real-valued clock variables to all
real-valued variables whose trajectories can be characterized using
piecewise-linear envelopes [20]. If the guarded assignments and
invariants of hybrid automata are linear constraints on continuous states,
and the differential equations are replaced by linear constraints on first
derivatives, then we obtain the class of linear hybrid automata, which
can be analyzed fully automatically. A typical linear constraint on first
derivatives is a rectangular differential inclusion
, which can be used to model, for example, time measured by
clocks with bounded drift, or distance covered by vehicles with bounded
speed. The only computer package capable of dealing with the full class of
linear hybrid automata, HYTECH, is under development by one of our team
members [21].
For hybrid automata, verification or design for verification is a complex problem. In work in our group, we have produced interesting new approaches involving the use of game theory and differential inclusions. However, it is fair to say that the approaches have the following difficulties: