Some lessons from the HYTECH experience

T.A. Henzinger, J. Preussig, H. Wong Toi, in:, IEEE, 2001, pp. 2887–2892.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published
Author
; ;
Abstract
We provide an overview of the current status of HYTECH, and reflect on some of the lessons learned from our experiences with the tool. HYTECH is a symbolic model checker for mixed discrete-continuous systems that are modeled as automata with piecewise-constant polyhedral differential inclusions. The use of a formal input language and automated procedures for state-space traversal lay the foundation for formally verifying properties of hybrid dynamical systems. We describe some recent experiences analyzing three hybrid systems. We point out the successes and limitations of the tool. The analysis procedure has been extended in a number of ways to address some of the tool's shortcomings. We evaluate these extensions, and conclude with some desiderata for verification tools for hybrid systems.
Publishing Year
Date Published
2001-05-01
Volume
3
Page
2887 - 2892
Conference
CDC: Decision and Control
IST-REx-ID

Cite this

Henzinger TA, Preussig J, Wong Toi H. Some lessons from the HYTECH experience. In: Vol 3. IEEE; 2001:2887-2892. doi:10.1109/.2001.980714
Henzinger, T. A., Preussig, J., & Wong Toi, H. (2001). Some lessons from the HYTECH experience (Vol. 3, pp. 2887–2892). Presented at the CDC: Decision and Control, IEEE. https://doi.org/10.1109/.2001.980714
Henzinger, Thomas A, Joerg Preussig, and Howard Wong Toi. “Some Lessons from the HYTECH Experience,” 3:2887–92. IEEE, 2001. https://doi.org/10.1109/.2001.980714.
T. A. Henzinger, J. Preussig, and H. Wong Toi, “Some lessons from the HYTECH experience,” presented at the CDC: Decision and Control, 2001, vol. 3, pp. 2887–2892.
Henzinger TA, Preussig J, Wong Toi H. 2001. Some lessons from the HYTECH experience. CDC: Decision and Control vol. 3. 2887–2892.
Henzinger, Thomas A., et al. Some Lessons from the HYTECH Experience. Vol. 3, IEEE, 2001, pp. 2887–92, doi:10.1109/.2001.980714.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar