TY - GEN
T1 - Computing bounded reach sets from sampled simulation traces
AU - Huang, Zhenqi
AU - Mitra, Sayan
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
KW - Hybrid automata
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=84860630153&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84860630153&partnerID=8YFLogxK
U2 - 10.1145/2185632.2185676
DO - 10.1145/2185632.2185676
M3 - Conference contribution
AN - SCOPUS:84860630153
SN - 9781450312202
T3 - HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control
SP - 291
EP - 294
BT - HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems
T2 - 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'12
Y2 - 17 April 2012 through 19 April 2012
ER -