HyLAA: a tool for computing simulation-equivalent reachability for linear systems. Simulations are a practical method of increasing the confidence that a system design is correct. This paper presents techniques which aim to determine all the states that can be reached using a particular hybrid automaton simulation algorithm, a property we call simulation-equivalent reachability. Although this is a slightly weaker property than traditional reachability, its computation can be efficient and accurate. We present HyLAA, the first tool for simulation-equivalent reachability for hybrid automata with affine dynamics. HyLAA’s analysis is exact; upon completion, the tool provides a concrete simulation trace to an unsafe state if and only if the hybrid automaton simulation engine could produce such a trace. In the backend, the tool implements an efficient algorithm for continuous post that exploits the superposition principle of linear systems, requiring only n+1 simulations per mode for an n-dimensional linear system. This technique is capable of analyzing a replicated helicopter system with over 1000 state variables in less than 20 minutes. The tool also contains several novel performance enhancements, such as invariant constraint elimination, warm-start linear programming, and trace-guided set deaggregation.
Keywords for this software
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Goyal, Manish; Duggirala, Parasara Sridhar: Extracting counterexamples induced by safety violation in linear hybrid systems (2020)
- Bak, Stanley; Bogomolov, Sergiy; Althoff, Matthias: Time-triggered conversion of guards for reachability analysis of hybrid automata (2017)