HYTECH: the next generation
Authors:
- T.A. HenzingerTHT.A. Henzinger
- Pei-Hsin HoPHPei-Hsin Ho
- H. Wong-ToiHWH. Wong-Toi
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 56-65
Abstract
We describe a new implementation of HYTECH, a symbolic model checker for hybrid systems. Given a parametric description of an embedded system as a collection of communicating automata, HYTECH automatically computes the conditions on the parameters under which the system satisfies its safety and timing requirements. While the original HYTECH prototype was based on the symbolic algebra tool Mathematica, the new implementation is written in C++ and builds on geometric algorithms instead of formula manipulation. The new HYTECH offers a cleaner and more expressive input language, greater portability, superior performance (typically two to three orders of magnitude), and new features such as diagnostic error-trace generation. We illustrate the effectiveness of the new implementation by applying HYTECH to the automatic parametric analysis of the generic railroad crossing benchmark problem and to an active structure control algorithm.Keywords
This publication has 20 references indexed in Scilit:
- A verifier for distributed real-time systems with bounded integer variables2002
- Automatic symbolic verification of embedded systems2002
- What's decidable about hybrid automata?1995
- Verification of linear hybrid systems by means of convex approximations1994
- The generalized railroad crossing: a case study in formal verification of real-time systems1994
- Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems1993
- An old-fashioned recipe for real time1992
- A proof system for communicating shared resources1990
- Automatic discovery of linear restraints among variables of a program1978
- Algorithm for discovering the set of all the solutions of a linear programming problemUSSR Computational Mathematics and Mathematical Physics, 1968