Computing bounded reach sets from sampled simulation traces

Zhenqi Huang, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationHSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control
Pages291-294
Number of pages4
DOIs
StatePublished - May 10 2012
Event15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'12 - Beijing, China
Duration: Apr 17 2012Apr 19 2012

Publication series

NameHSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control

Other

Other15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'12
CountryChina
CityBeijing
Period4/17/124/19/12

Keywords

  • Hybrid automata
  • Verification

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Computer Science Applications

Fingerprint Dive into the research topics of 'Computing bounded reach sets from sampled simulation traces'. Together they form a unique fingerprint.

Cite this