TY - GEN
T1 - Locally optimal reach set over-approximation for nonlinear systems
AU - Fan, Chuchu
AU - Kapinski, James
AU - Jin, Xiaoqing
AU - Mitra, Sayan
N1 - grant CCF 1422798 from the National Science Foundation.
PY - 2016/10/1
Y1 - 2016/10/1
N2 - 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∗.
AB - 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∗.
UR - http://www.scopus.com/inward/record.url?scp=84995479980&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84995479980&partnerID=8YFLogxK
U2 - 10.1145/2968478.2968482
DO - 10.1145/2968478.2968482
M3 - Conference contribution
AN - SCOPUS:84995479980
T3 - Proceedings of the 13th International Conference on Embedded Software, EMSOFT 2016
BT - Proceedings of the 13th International Conference on Embedded Software, EMSOFT 2016
PB - Association for Computing Machinery
T2 - 13th International Conference on Embedded Software, EMSOFT 2016
Y2 - 1 October 2016 through 7 October 2016
ER -