Some lessons from the HYTECH experience
Proceedings of the 40th IEEE Conference on Decision and Control (Cat. No.01CH37228)Published 10 July 2003
Thomas A. Henzinger, Jörg Preußig, Howard Wong-Toi
Citations44
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
An overview of the current status of HYTECH, some recent experiences analyzing three hybrid systems, and some desiderata for verification tools for hybrid systems are described.
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.
Keywords
Computer Science
Theoretical Computer ScienceThe algorithmic analysis of hybrid systems
1,868 Citations1995Rajeev Alur, Costas Courcoubetis +7 more
A general framework for the formal specification and algorithmic analysis of hybrid systems is presented, which considers symbolic model-checking and minimization procedures that are based on the reachability analysis of an infinite state space.
Lecture notes in computer scienceApproximate Reachability Analysis of Piecewise-Linear Dynamical Systems
338 Citations2000Eugène Asarin, Olivier Bournez +2 more
An experimental system called d/dt for approximating reachable states for hybrid systems whose continuous dynamics is defined by linear differential equations using an approximation algorithm whose accumulation of errors during the continuous evolution is much smaller than in previously-used methods.
Lecture notes in computer scienceA user guide to HyTech
246 Citations1995Thomas A. Henzinger, Pei -Hsin Ho +1 more
This guide gives several examples of usage, some hints for gaining maximal computational efficiency from the tool, and the complete grammar for the input language for describing and analyzing systems.
Lecture notes in computer scienceLevel Set Methods for Computation in Hybrid Systems
231 Citations2000Ian M. Mitchell, Claire J. Tomlin
This work presents an implementation of an exact reachability operator for nonlinear hybrid systems, and an equivalent formulation is developed of the key equations governing the continuous state reachability.
Lecture notes in computer scienceVerification of Polyhedral-Invariant Hybrid Automata Using Polygonal Flow Pipe Approximations
228 Citations1999Alongkrit Chutinan, Bruce H. Krogh
The paper presents an application of the computational procedure to a benchmark hybrid system, a batch evaporator, and the fundamental computation in the generation of approximating automata is the mapping of sets of continuous states to the boundaries of the location invariants.
Lecture notes in computer scienceModular Specification of Hybrid Systems in Charon
175 Citations2000Rajeev Alur, Radu Grosu +3 more
A scheme for modular simulation in which each mode can be compiled solely based on the locally declared information to execute its discrete and continuous updates, and furthermore, submodes can integrate at a finer time scale than the enclosing modes.
Lecture notes in computer scienceAutomatic Verification of Parameterized Cache Coherence Protocols
148 Citations2000Giorgio Delzanno
With this application, it is shown that symbolic model checking tools originally designed for hybrid and concurrent systems can be applied successfully to a new class of infinite-state systems of practical interest.
Lecture notes in computer scienceVerification of Hybrid Systems with Linear Differential Inclusions Using Ellipsoidal Approximations
148 Citations2000Oleg Botchkarev, Stavros Tripakis
A general verification algorithm is described and it is shown how ellipsoidal methods developed by A. Kurzhanski and P. Varaiya can be adapted to the algorithm and implemented in the verification tool called VeriSHIFT.
Lecture notes in computer scienceBeyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods
144 Citations2000Thomas A. Henzinger, Benjamin Horowitz +2 more
A new algorithm is designed, capable of directly verifying hybrid systems with general continuous dynamics, such as linear and nonlinear differential equations, and is implemented in a successor tool to HyTech called HyperTech, which enables the direct, fully automatic analysis of these systems.
Lecture notes in computer scienceDelay analysis in synchronous programs
135 Citations1993Nicolas Halbwachs
This work proposes to apply linear relation analysis to variables used to count delays in synchronous programs, and finds that the results can be applied to code optimization and to the verification of real-time properties of programs.
Lecture notes in computer scienceAutomated analysis of an audio control protocol
86 Citations1995Pei -Hsin Ho, Howard Wong-Toi
HyTech, a symbolic model checker for linear hybrid systems, can be used to analyze an audio control protocol and can automatically synthesize the bound on the maximum clock drift, and suggest design modification for a more robust protocol.
Cut-off in engine control: a hybrid system approach
79 Citations2002A. Balluchi, Maria Domenica Di Benedetto +3 more
A novel approach to the control of an automotive engine in the cut-off region is presented, which is formulated as a hybrid optimization problem, whose solution is obtained by relaxing it to the continuous domain and mapping its solution back into the hybrid domain.
Lecture notes in computer scienceAssume-Guarantee Reasoning for Hierarchical Hybrid Systems
77 Citations2001Thomas A. Henzinger, Marius Minea +1 more
This work presents a model for hierarchical system design which permits the arbitrary nesting of parallel as well as serial composition, and which supports an assume-guarantee principle for mixed parallel-serial contexts.
Lecture notes in computer scienceUsing HyTech to synthesize control parameters for a steam boiler
74 Citations1996Thomas A. Henzinger, Howard Wong-Toi
This work model a steam-boiler control system using hybrid automata and provides two abstracted linear models of the nonlinear behavior of the boiler, which permits the design of a more efficient controller.
IEEE Transactions on Software EngineeringTiming analysis of Ada tasking programs
66 Citations1996James C. Corbett
This paper provides a method for building mathematical models of real-time Ada tasking programs that are accurate enough to verify interesting timing properties, and yet abstract enough to yield a tractable analysis on nontrivial programs.
Lecture notes in computer scienceUsing HyTech to verify an automotive control System
62 Citations1997Thomas Stauner, Olaf Müller +1 more
HyTech, a symbolic model checker for linear hybrid systems, can be used to verify a part of an abstracted automotive control system, and a property related to stability in the sense of control theory is verified.
Lecture notes in computer scienceA Case Study in Tool-Aided Analysis of Discretely Controlled Continuous Systems: The Two Tanks Problem
60 Citations1999Stefan Kowalewski, Olaf Stursberg +7 more
This case study compares the usefulness and applicability of eight computer tools with respect to the validation of logic control programs for continuous processes with emphasis on the suitability to the problem and the numerical performance.
Formal verification of hybrid systems using CheckMate: a case study
59 Citations2000B.I. Silva, Bruce H. Krogh
This case study illustrates how verification can be performed directly on a model of the hybrid system dynamics without first constructing an approximation to the continuous dynamics using timed automata or linear hybrid automata models.
Lecture notes in computer scienceA note on abstract interpretation strategies for hybrid automata
58 Citations1995Thomas A. Henzinger, Pei-Hsin Ho
Several abstract interpretation strategies that are designed to improve the performance of HyTech, a symbolic model checker for linear hybrid systems are reported on.
Lecture notes in computer scienceReachability Analysis of (Timed) Petri Nets Using Real Arithmetic
46 Citations1999Béatrice Bérard, Laurent Fribourg
It is shown that exact reachability analysis can be achieved by treating Petri nets integer variables (counters) as real-valued variables, and using Fourier-Motzkin procedure instead of Presburger elimination procedure, and can be safely analysed with performant tools, e.g. HyTech.
Formal Aspects of ComputingA formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
45 Citations1994J Strother Moore
This paper develops part of the reusable formal theory that permits the convenient application of the model of asynchronous communication as a function in the Boyer-Moore logic and uses the theory to show that a biphase mark protocol can be used to send messages of arbitrary length between two asynchronous processors.
Lecture notes in computer scienceReachability Analysis of a Class of Switched Continuous Systems by Integrating Rectangular Approximation and Rectangular Analysis
29 Citations1999Jörg Preußig, Olaf Stursberg +1 more
In the presented procedure the flow conditions of the visited locations are determinded on-the-fly during the course of the analysis of the reachability analysis of switched continuous systems in which switching only occurs when the continuous state trajectory crosses thresholds defined by a rectangular partitioning of the state space.
Lecture notes in computer scienceAn algorithm for the approximative analysis of rectangular automata
27 Citations1998Jörg Preuig, Stefan Kowalewski +2 more
This paper presents an analysis algorithm that uses conservative overapproximation to avoid severe numerical problems for even medium-sized systems.
Lecture notes in computer scienceAutomated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol
27 Citations1999Béeatrice Béerard, Laurent Fribourg
A modelization of the ABR conformance protocol, using parametric timed automata, and the tool HyTech is used for computing the set of reachable states of the model, and automatically proving the property of reachability.
IEEE Transactions on Software EngineeringAnalyzing partially-implemented real-time systems
16 Citations1998George S. Avrunin, James C. Corbett +1 more
Lecture notes in computer scienceTowards Using Hybrid Automata for the Mission Planning of Unmanned Aerial Vehicles
15 Citations1999Conrado W. Seibel, Jean-Marie Farines +1 more
This paper describes a methodology for the design of flight plans for rotary-wing unmanned aerial vehicles based on formal verification which greatly reduces the time needed to plan a mission and increases the safety of the aircraft's operation.
Formal verification of an automotive engine controller in cutoff mode
10 Citations2002Tiziano Villa, Howard Wong-Toi +4 more
Formal verification of convergence and performance properties of an engine control algorithm being developed for Magneti-Marelli is described and the sliding action of the hybrid controller is formally verified with the model checker HYTECH.
Lecture notes in computer scienceScheduling System Verification
6 Citations1999Pao‐Ann Hsiung, Farn Wang +1 more
A formal framework is proposed for the verification of complex real-time systems, modeled as client-server scheduling systems, using the popular model-checking approach, with wide-applicability, significant state-space reduction, and several scheduling semantics.
A procedure for reachability analysis of rectangular automata
5 Citations2000Howard Wong-Toi, Jörg Preußig
A procedure for the reachability analysis of rectangular automata, with the main restriction being that all derivatives, guards, and invariants are defined by constant lower and upper bounds in each dimension.
Computers & Chemical EngineeringUsing model-checking for timed automata to parameterize logic control programs
5 Citations1998Stefan Kowalewski, Sebastian Engell +4 more
The modeling and analysis framework of Timed Automata can be used to determine valid parameter ranges for timers in logic control programs by means of a simple process engineering example.
Modular verification of a fault-tolerant active structure controller: an example
1 Citations2003Howard Wong-Toi
This work provides the first known nontrivial application of modular verification in conjunction with the model-checking paradigm for verifying hybrid systems, and verifies a fault-tolerant active structure control system.