HYTECH: the next generation
- 19 November 2002
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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 variablesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Automatic symbolic verification of embedded systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- What's decidable about hybrid automata?Published by Association for Computing Machinery (ACM) ,1995
- Verification of linear hybrid systems by means of convex approximationsLecture Notes in Computer Science, 1994
- The generalized railroad crossing: a case study in formal verification of real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1994
- Hybrid automata: An algorithmic approach to the specification and verification of hybrid systemsLecture Notes in Computer Science, 1993
- An old-fashioned recipe for real timePublished by Springer Science and Business Media LLC ,1992
- A proof system for communicating shared resourcesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Automatic discovery of linear restraints among variables of a programPublished by Association for Computing Machinery (ACM) ,1978
- Algorithm for discovering the set of all the solutions of a linear programming problemUSSR Computational Mathematics and Mathematical Physics, 1968