Locally Optimal Reach Set Over-approximation for Nonlinear Systems

Fan, Chuchu; Kapinski, James; Jin, Xiaoqing; Mitra, Sayan

Permalink

https://hdl.handle.net/2142/90424 Copy

Description

Title

Locally Optimal Reach Set Over-approximation for Nonlinear Systems

Author(s)

• Fan, Chuchu
• Kapinski, James
• Jin, Xiaoqing
• Mitra, Sayan

Issue Date

2016-07-05

Keyword(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*.

Publisher

Coordinated Science Laboratory, University of Illinois at Urbana-Champaign

Series/Report Name or Number

Coordinated Science Laboratory Report no. UILU-ENG-16-2202

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/90424

Sponsor(s)/Grant Number(s)

National Science Foundation/CCF 1422798

Owning Collections