|
HyTech: The HYbrid TECHnology Tool
HyTech is an automatic tool for the analysis of embedded systems.
HyTech computes the condition under which a linear hybrid system satisfies
a temporal requirement.
Hybrid systems are specified as collections of automata with discrete and
continuous components, and temporal requirements are verified by symbolic
model checking.
If the verification fails, then HyTech generates a diagnostic error trace.
The standard reference to the HyTech algorithm is [1], and the standard
reference to the HyTech tool, [2].
[1] R. Alur, T.A. Henzinger, and P.-H. Ho.
Automatic Symbolic Verification of Embedded Systems.
IEEE Transactions on Software Engineering 22:181-201, 1996.
[2] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi.
HyTech: A Model Checker for Hybrid Systems.
Software Tools for Technology Transfer 1:110-122, 1997.
The HyTech Team
HyTech was developed by
Tom Henzinger,
Pei-Hsin Ho,
and
Howard Wong-Toi.
The HyTech Papers
The HyTech Files
-
User guide: a manual with instructions for installation and usage
-
License agreement: we ask you to submit this before you get the software
-
hytech.tar.gz: HyTech Version 1.04f (Gzip compressed tar file of 679 KB)
-
hytech.tgz: the same as above (for users of Windows, which has a
problem with multiple file extensions)
The file hytech.tar.gz contains all source files and a Linux executable (hytech.exe).
We have compiled the same sources under Windows 2000 with Cygwin.
The source files have been compiled also under Sun OS 5.8, Solaris 2.3.x, Digital Unix, DEC Ultrix,
HP-UX, and Windows 2000 (Cygwin).
The resulting binaries have been compressed with gzip and uuencoded.
Select the appropriate file to download for your system,
"hytech-v1.04a-myOS.exe" say. Save it as the file "hytech.uu". Uudecode this file, then
uncompress it. For example, under Unix, use the commands "uudecode" followed by
"gunzip". This procedure will give you a binary that should be renamed "hytech.exe"
and placed on your command path. Unfortunately, I do not have access to some machine configurations
any more, so some of the
executables below are for older versions of the source code. However, you should be
able to compile the sources yourself with little effort.
See the user guide for installation instructions.
Two HyTech Case Studies
A Graphical User Interface
A graphical input language for HyTech is now available courtesy of the
Uppaal group in Denmark and Sweden:
For questions and comments send mail to
hytech@eecs.berkeley.edu
Tom Henzinger: back to my
home page
Last updated in February, 2003.
|
