## Beyond HyTech:
Hybrid Systems Analysis Using Interval Numerical Methods

*
Thomas A. Henzinger,
Benjamin Horowitz, Rupak Majumdar, and Howard Wong-Toi*

Since hybrid embedded systems are pervasive and often safety-critical,
guarantees about their correct performance are desirable. The hybrid systems
model checker HyTech provides such guarantees and has successfully verified
some systems. However, HyTech severely restricts the continuous dynamics of
the system being analyzed and, therefore, often forces the use of
prohibitively expensive discrete and polyhedral abstractions. We have
designed a new algorithm, which is capable of directly verifying hybrid
systems with general continuous dynamics, such as linear and nonlinear
differential equations. The new algorithm conservatively overapproximates
the reachable states of a hybrid automaton by using interval numerical
methods. Interval numerical methods return sets of points that enclose the
true result of numerical computation and, thus, avoid distortions due to the
accumulation of round-off errors. We have implemented the new algorithm in a
successor tool to HyTech called HyperTech. We consider three examples: a
thermostat with delay, a two-tank water system, and an air-traffic collision
avoidance protocol. HyperTech enables the direct, fully automatic analysis
of these systems, which is also more accurate than the use of polyhedral
abstractions.

*Proceedings of the
Third International Workshop on Hybrid Systems: Computation and Control*
(HSCC),
Lecture Notes in Computer Science 1790,
Springer, 2000, pp. 130-144.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2000 Springer.