Files in this item



application/pdfUILU-ENG-16-2202.pdf (518kB)
(no description provided)PDF


Title:Locally Optimal Reach Set Over-approximation for Nonlinear Systems
Author(s):Fan, Chuchu; Kapinski, James; Jin, Xiaoqing; Mitra, Sayan
Subject(s):Formal verification
Embedded systems
Matrix measure
Reachability algorithms
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 applicable only to 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*.
Issue Date:2016-07-05
Publisher:Coordinated Science Laboratory
Citation Info:Chuchu Fan, James Kapinski, Xiaoqing Jin, and Sayan Mitra, "Locally Optimal Reach Set Over-approximation for Nonlinear Systems," Coordinated Science Laboratory technical report no. UILU-ENG-16-2202, University of Illinois at Urbana-Champaign, July 2016.
Coordinated Science Laboratory Report no. UILU-ENG-16-2202
Genre:Technical Report
Sponsor:National Science Foundation/CCF 1422798
Date Available in IDEALS:2016-07-05

This item appears in the following Collection(s)

Item Statistics