Beyond HyTech: Hybrid systems analysis using interval numerical methods

Henzinger TA, Horowitz B, Majumdar R, Wong Toi H. 2000. Beyond HyTech: Hybrid systems analysis using interval numerical methods. Proceedings of the 3rd International Workshop on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 1790, 130–144.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published | English

Scopus indexed
Author
Henzinger, Thomas AISTA ; Horowitz, Benjamin; Majumdar, Ritankar; Wong Toi, Howard
Series Title
LNCS
Abstract
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.
Publishing Year
Date Published
2000-01-01
Proceedings Title
Proceedings of the 3rd International Workshop on Hybrid Systems: Computation and Control
Acknowledgement
This research was supported in part by the DARPA (NASA) grant NAG2-1214, the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.
Volume
1790
Page
130 - 144
Conference
HSCC: Hybrid Systems - Computation and Control
Conference Location
Pittsburgh, PA, United States of America
Conference Date
2000-03-23 – 2000-03-25
IST-REx-ID

Cite this

Henzinger TA, Horowitz B, Majumdar R, Wong Toi H. Beyond HyTech: Hybrid systems analysis using interval numerical methods. In: Proceedings of the 3rd International Workshop on Hybrid Systems: Computation and Control. Vol 1790. Springer; 2000:130-144. doi:10.1007/3-540-46430-1_14
Henzinger, T. A., Horowitz, B., Majumdar, R., & Wong Toi, H. (2000). Beyond HyTech: Hybrid systems analysis using interval numerical methods. In Proceedings of the 3rd International Workshop on Hybrid Systems: Computation and Control (Vol. 1790, pp. 130–144). Pittsburgh, PA, United States of America: Springer. https://doi.org/10.1007/3-540-46430-1_14
Henzinger, Thomas A, Benjamin Horowitz, Ritankar Majumdar, and Howard Wong Toi. “Beyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods.” In Proceedings of the 3rd International Workshop on Hybrid Systems: Computation and Control, 1790:130–44. Springer, 2000. https://doi.org/10.1007/3-540-46430-1_14.
T. A. Henzinger, B. Horowitz, R. Majumdar, and H. Wong Toi, “Beyond HyTech: Hybrid systems analysis using interval numerical methods,” in Proceedings of the 3rd International Workshop on Hybrid Systems: Computation and Control, Pittsburgh, PA, United States of America, 2000, vol. 1790, pp. 130–144.
Henzinger TA, Horowitz B, Majumdar R, Wong Toi H. 2000. Beyond HyTech: Hybrid systems analysis using interval numerical methods. Proceedings of the 3rd International Workshop on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 1790, 130–144.
Henzinger, Thomas A., et al. “Beyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods.” Proceedings of the 3rd International Workshop on Hybrid Systems: Computation and Control, vol. 1790, Springer, 2000, pp. 130–44, doi:10.1007/3-540-46430-1_14.

Export

Marked Publications

Open Data ISTA Research Explorer

Search this title in

Google Scholar
ISBN Search