Locally optimal reach set over-approximation for nonlinear systems

Chuchu Fan, James Kapinski, Xiaoqing Jin, Sayan Mitra

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

Abstract

Safety verification of embedded systems modeled as hybrid systems can be scaled up by employing simulation-guided reach set over-approximation techniques. Existing methods are either applicable to only restricted classes of systems, overly conservative, or computationally expensive. We present new techniques to compute a locally optimal bloating factor based on discrepancy functions, which allow construction of reach set over-approximations from simulation traces for general nonlinear systems. The discrepancy functions are critical for tools like C2E2 to verify bounded time safety properties for complex hybrid systems with nonlinear continuous dynamics. The new discrepancy function is computed using local bounds on a matrix measure under an optimal metric such that the exponential change rate of the discrepancy function is minimized. The new technique is less time consuming and less conservative than existing techniques and does not incur significant computational overhead. We demonstrate the effectiveness of our approach by comparing the performance of a prototype implementation with the state-of-the-art reachability analysis tool Flow∗.

Original languageEnglish (US)
Title of host publicationProceedings of the 13th International Conference on Embedded Software, EMSOFT 2016
PublisherAssociation for Computing Machinery, Inc
ISBN (Electronic)9781450344852
DOIs
StatePublished - Oct 1 2016
Event13th International Conference on Embedded Software, EMSOFT 2016 - Pittsburgh, United States
Duration: Oct 1 2016Oct 7 2016

Publication series

NameProceedings of the 13th International Conference on Embedded Software, EMSOFT 2016

Other

Other13th International Conference on Embedded Software, EMSOFT 2016
CountryUnited States
CityPittsburgh
Period10/1/1610/7/16

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Locally optimal reach set over-approximation for nonlinear systems'. Together they form a unique fingerprint.

Cite this