Hybrid Trace Verifier

swMATH ID: 20335
Software Authors: Huang, Zhenqi; Mitra, Sayan
Description: Computing bounded reach sets from sampled simulation traces. This paper presents an algorithm which uses simulation traces and formal models for computing overapproximations of reach sets of deterministic hybrid systems. The implementation of the algorithm in a tool, Hybrid Trace Verifier (HTV), uses Mathwork’s Simulink/Stateflow (SLSF) environment for generating simulation traces and for obtaining formal models. Computation of the overapproximation relies on computing error bounds in the dynamics obtained from the formal model. Verification results from three case studies, namely, a version of the navigation benchmark, an engine control system, and a satellite system suggest that this combined formal analysis and simulation based approach may scale to larger problems.
Homepage: http://dl.acm.org/citation.cfm?doid=2185632.2185676
Keywords: hybrid system; verification
Related Software: GRKLib; S-TaLiRo; StateFlow; Simulink; Breach; C2e2; dde23; CAPD; DDE-BIFTOOL
Cited in: 2 Publications

Citations by Year