Beyond HYTECH: Hybrid Systems Analysis Using Interval Numerical Methods

Abstract. Sincehybridembeddedsystemsarepervasiveandoftensafetycritical, guarantees about their correct performance are desirable. The hybrid systemsmodelcheckerHyTech providessuch guaranteesand has successfully veri ed some systems. However, HyTech severely restricts the continuous dynamics of the system being analyzed and, therefore, often forces the use of prohibitively expensive discrete and polyhedral abstractions. We have designed a new algorithm, which is capable of directly verifying hybrid systems with general continuous dynamics, such as linear and nonlinear di erential equations. The new algorithm conservatively overapproximates the reachable states of a hybrid automaton by using interval numerical methods. Interval numerical methods return sets of points that enclose the true result of numerical computation and, thus, avoid distortions due to the accumulation of round-o errors. We have implemented the new algorithm in a successor tool to HyTech called HyperTech. We consider ...

• Type: Conference
• Year: 2000
• Where: HYBRID
• Authors: Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar, Howard Wong-Toi
• Keywords: Continuous Dynamics, Control Systems, HYBRID 2000, Interval Numerical Methods, SystemsmodelcheckerHyTech Providessuch Guaranteesand