More Web Proxy on the site http://driver.im/

research-article

Falsification of hybrid systems using symbolic reachability and trajectory splicing

Authors:

Sergiy Bogomolov,

Rajarshi RayAuthors Info & Claims

HSCC '19: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control

Pages 1 - 10

https://doi.org/10.1145/3302504.3311813

Published: 16 April 2019 Publication History

Abstract

The falsification of a hybrid system aims at finding trajectories that violate a given safety property. This is a challenging problem, and the practical applicability of current falsification algorithms still suffers from their high time complexity. In contrast to falsification, verification algorithms aim at providing guarantees that no such trajectories exist. Recent symbolic reachability techniques are capable of efficiently computing linear constraints that enclose all trajectories of the system with reasonable precision. In this paper, we leverage the power of symbolic reachability algorithms to improve the scalability of falsification techniques. Recent approaches to falsification reduce the problem to a nonlinear optimization problem. We propose to reduce the search space of the optimization problem by adding linear state constraints obtained with a reachability algorithm. We showcase the efficiency of our approach on a number of standard hybrid systems benchmarks demonstrating the performance increase in speed and number of falsifyable instances.

References

[1]

Matthias Althoff, Olaf Stursberg, and Martin Buss. 2010. Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes. Nonlinear analysis: hybrid systems 4, 2 (2010), 233--249.

[2]

R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. 1995. The algorithmic analysis of hybrid systems. Theoretical Computer Science 138, 1 (1995), 3--34.

Digital Library

[3]

Yashwanth Singh Rahul Annapureddy, Che Liu, Georgios E. Fainekos, and Sriram Sankaranarayanan. 2011. S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In Tools and algorithms for the construction and analysis of systems (LNCS), Vol. 6605. Springer, 254--257. https://sites.google.com/a/asu.edu/s-taliro/.

Digital Library

[4]

C. Wouter Bac, Tim Roorda, Roi Reshef, Sigal Berman, Jochen Hemming, and Eldert J. van Henten. 2016. Analysis of a motion planning problem for sweet-pepper harvesting in a dense obstacle environment. Biosystems Engineering 146 (2016), 85--97. Special Issue: Advances in Robotic Agriculture for Crops.

[5]

Stanley Bak, Sergiy Bogomolov, Thomas A. Henzinger, and Aviral Kumar. 2017. Challenges and Tool Implementation of Hybrid Rapidly-Exploring Random Trees. In International Workshop on Numerical Software Verification. Springer.

[6]

Stanley Bak and Parasara Sridhar Duggirala. 2017. Hylaa: A tool for computing simulation-equivalent reachability for linear systems. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control. ACM, 173--178.

Digital Library

[7]

I. Ben Makhlouf and S. Kowalewski. 2015. Networked Cooperative Platoon of Vehicles for Testing Methods and Verification Tools. In Proc. of ARCH14--15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems. 37--42.

[8]

Dimitri P Bertsekas. 1999. Nonlinear programming. Athena scientific Belmont.

[9]

H.G. Bock and K.J. Plitt. 1984. A Multiple Shooting Algorithm for Direct Solution of Optimal Control Problems*. IFAC Proceedings Volumes 17, 2 (1984), 1603--1608. 9th IFAC World Congress: A Bridge Between Control Science and Technology, Budapest, Hungary, 2--6 July 1984.

[10]

Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Frédéric Viry, Andreas Podelski, and Christian Schilling. 2018. Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week). ACM, 41--50.

Digital Library

[11]

Sergiy Bogomolov, Daniele Magazzeni, Stefano Minopoli, and Martin Wehrle. 2015. PDDL+ Planning with Hybrid Automata: Foundations of Translating Must Behavior. In ICAPS. 42--46.

Digital Library

[12]

Sergiy Bogomolov, Daniele Magazzeni, Andreas Podelski, and Martin Wehrle. 2014. Planning as Model Checking in Hybrid Domains. In AAAI. 2228--2234.

Digital Library

[13]

Amanda Jane Coles, Andrew I Coles, Maria Fox, and Derek Long. 2012. COLIN: Planning with continuous linear numeric change. Journal of Artificial Intelligence Research 44 (2012), 1--96.

Digital Library

[14]

Adel Dokhanchi, Shakiba Yaghoubi, Bardh Hoxha, Georgios Fainekos, Gidon Ernst, Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo, and Sean Sedwards. 2018. ARCH-COMP18 Category Report: Results on the Falsification Benchmarks. In ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems (EPiC Series in Computing), Goran Frehse and Matthias Althoff (Eds.), Vol. 54. EasyChair, 104--109. FalStar : https://github.com/ERATOMMSD/.

[15]

Alexandre Donzé. 2010. Breach, a toolbox for verification and parameter synthesis of hybrid systems. In International Conference on Computer Aided Verification. Springer, 167--170. Breach : https://github.com/decyphir/breach.

Digital Library

[16]

Ansgar Fehnker and Franjo Ivancic. 2004. Benchmarks for Hybrid Systems Verification. In HSCC (Lecture Notes in Computer Science), Rajeev Alur and George J. Pappas (Eds.), Vol. 2993. Springer, 326--341.

[17]

Maria Fox and Derek Long. 2002. PDDL+: Modeling continuous time dependent effects. In Proceedings of the 3rd International NASA Workshop on Planning and Scheduling for Space, Vol. 4. 34.

[18]

Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable Verification of Hybrid Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV) (LNCS), Shaz Qadeer Ganesh Gopalakrishnan (Ed.). Springer. http://spaceex.imag.fr.

Digital Library

[19]

Jonathan D Gammell, Siddhartha S Srinivasa, and Timothy D Barfoot. 2014. Informed RRT*: Optimal sampling-based path planning focused via direct sampling of an admissible ellipsoidal heuristic. In IEEE/RSJ International Conference on Intelligent Robots and Systems. 2997--3004.

[20]

Colas Le Guernic and Antoine Girard. 2009. Reachability Analysis of Hybrid Systems Using Support Functions. In CAV (Lecture Notes in Computer Science), Ahmed Bouajjani and Oded Maler (Eds.), Vol. 5643. Springer, 540--554.

Digital Library

[21]

Steven G. Johnson. 2018. The NLopt nonlinear-optimization package. http://ab-initio.mit.edu/nlopt.

[22]

James J. Kuffner and Steven M. LaValle. 2000. RRT-Connect: An Efficient Approach to Single-Query Path Planning. In ICRA.

[23]

Jan Kuřátko and Stefan Ratschan. 2014. Combined global and local search for the falsification of hybrid systems. In International Conference on Formal Modeling and Analysis of Timed Systems. Springer, 146--160.

[24]

Steven M LaValle. 1998. Rapidly-exploring random trees: A new tool for path planning. (1998).

[25]

Steven M LaValle and James J Kuffner Jr. 2001. Randomized kinodynamic planning. The international journal of robotics research 20, 5 (2001), 378--400.

[26]

Colas Le Guernic and Antoine Girard. 2010. Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems 4, 2 (2010), 250--262.

[27]

Giuseppe Della Penna, Daniele Magazzeni, Fabio Mercorio, and Benedetto Intrigila. 2009. UPMurphi: A Tool for Universal Planning on PDDL+ Problems. In ICAPS.

[28]

Wiktor Mateusz Piotrowski, Maria Fox, Derek Long, Daniele Magazzeni, and Fabio Mercorio. 2016. Heuristic Planning for PDDL+ Domains.

[29]

Rajarshi Ray, Amit Gurung, Binayak Das, Ezio Bartocci, Sergiy Bogomolov, and Radu Grosu. 2015. XSpeed: Accelerating Reachability Analysis on Multi-core Processors. In Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, HVC 2015, Proceedings (Lecture Notes in Computer Science), Nir Piterman (Ed.), Vol. 9434. Springer, 3--18. http://xspeed.nitmeghalaya.in.

[30]

Enrico Scala, Patrik Haslum, Sylvie Thiébaux, and Miquel Ramirez. 2016. Interval-Based Relaxation for General Numeric Planning. In ECAI. 655--663.

Digital Library

[31]

Krister Svanberg. 1987. The method of moving asymptotes - a new method for structural optimization. International journal for numerical methods in engineering 24, 2 (1987), 359--373.

[32]

Gu Ye and Ron Alterovitz. 2017. Guided motion planning. In Robotics research. Springer, 291--307.

[33]

Aditya Zutshi, Jyotirmoy V Deshmukh, Sriram Sankaranarayanan, and James Kapinski. 2014. Multiple shooting, cegar-based falsification for hybrid systems. In Proceedings of the 14th International Conference on Embedded Software. ACM, 5.

Digital Library

[34]

Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy V. Deshmukh, and James Kapinski. 2013. A trajectory splicing approach to concretizing counterexamples for hybrid systems. In Proceedings of the 52nd IEEE Conference on Decision and Control, CDC 2013, December 10--13, 2013. 3918--3925.

Cited By

Sheikhi SDuggirala PBak S(2024)Testing Autonomous Cyber-Physical Systems with Koopman Surrogate Model Predictive Control2024 IEEE 10th International Conference on Space Mission Challenges for Information Technology (SMC-IT)10.1109/SMC-IT61443.2024.00018(99-108)Online publication date: 15-Jul-2024
https://doi.org/10.1109/SMC-IT61443.2024.00018
Wang JLiu WZhang MWei JShi YBu LLi X(2024)Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSsComputer Aided Verification10.1007/978-3-031-65633-0_15(329-355)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65633-0_15
Kundu ADas SRay R(2023) SAT-Reach: A Bounded Model Checker for Affine Hybrid SystemsACM Transactions on Embedded Computing Systems10.1145/356742522:2(1-36)Online publication date: 24-Jan-2023
https://dl.acm.org/doi/10.1145/3567425
Show More Cited By

Index Terms

Falsification of hybrid systems using symbolic reachability and trajectory splicing

Recommendations

Multiple shooting, CEGAR-based falsification for hybrid systems
EMSOFT '14: Proceedings of the 14th International Conference on Embedded Software

In this paper, we present an approach for finding violations of safety properties of hybrid systems. Existing approaches search for complete system trajectories that begin from an initial state and reach some unsafe state. We present an approach that ...
Predicate abstraction for reachability analysis of hybrid systems

Embedded systems are increasingly finding their way into a growing range of physical devices. These embedded systems often consist of a collection of software threads interacting concurrently with each other and with a physical, continuous environment. ...
Falsification of combined invariance and reachability specifications in hybrid control systems

We propose an abstraction-based method that can be applied to falsify a class of computation tree logic (CTL) specifications that combine invariance and reachability requirements in terms of the discrete state of a hybrid control system. The fragment of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '19: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control

April 2019

299 pages

ISBN:9781450362825

DOI:10.1145/3302504

Program Chairs:
Necmiye Ozay
University of Michigan
,
Pavithra Prabhakar
Kansas State University

Copyright © 2019 ACM.

Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of the United States government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 April 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

HSCC '19

Sponsor:

SIGBED

HSCC '19: 22nd ACM International Conference on Hybrid Systems: Computation and Control

April 16 - 18, 2019

Quebec, Montreal, Canada

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
388
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)3

Reflects downloads up to 22 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sheikhi SDuggirala PBak S(2024)Testing Autonomous Cyber-Physical Systems with Koopman Surrogate Model Predictive Control2024 IEEE 10th International Conference on Space Mission Challenges for Information Technology (SMC-IT)10.1109/SMC-IT61443.2024.00018(99-108)Online publication date: 15-Jul-2024
https://doi.org/10.1109/SMC-IT61443.2024.00018
Wang JLiu WZhang MWei JShi YBu LLi X(2024)Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSsComputer Aided Verification10.1007/978-3-031-65633-0_15(329-355)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65633-0_15
Kundu ADas SRay R(2023) SAT-Reach: A Bounded Model Checker for Affine Hybrid SystemsACM Transactions on Embedded Computing Systems10.1145/356742522:2(1-36)Online publication date: 24-Jan-2023
https://dl.acm.org/doi/10.1145/3567425
Kiviriga ALarsen KNickovic DNyman U(2023)Usage-and Risk-Aware Falsification Testing for Cyber-Physical SystemsFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-42626-1_9(141-157)Online publication date: 29-Aug-2023
https://doi.org/10.1007/978-3-031-42626-1_9
Clavière AAltieri Sambartolomé LAsselin EGarion CPagetti CBartocci EPutot S(2022)Verification of machine learning based cyber-physical systems: a comparative studyProceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3501710.3519540(1-16)Online publication date: 4-May-2022
https://dl.acm.org/doi/10.1145/3501710.3519540
Goyal MDewaskar MDuggirala P(2022)NExG: Provable and Guided State-Space Exploration of Neural Network Control Systems Using Sensitivity ApproximationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.319752441:11(4265-4276)Online publication date: Nov-2022
https://doi.org/10.1109/TCAD.2022.3197524
Wang JBu LXing SLi X(2022)PDF: Path-Oriented, Derivative-Free Approach for Safety Falsification of Nonlinear and Nondeterministic CPSIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2021.305636041:2(238-251)Online publication date: Feb-2022
https://doi.org/10.1109/TCAD.2021.3056360
Sheikhi SKim EDuggirala PBak S(2022)Coverage-Guided Fuzz Testing for Cyber-Physical Systems2022 ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS)10.1109/ICCPS54341.2022.00009(24-33)Online publication date: May-2022
https://doi.org/10.1109/ICCPS54341.2022.00009
Claviere AAsselin EGarion CPagetti C(2021)Safety Verification of Neural Network Controlled Systems2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W)10.1109/DSN-W52860.2021.00019(47-54)Online publication date: Jun-2021
https://doi.org/10.1109/DSN-W52860.2021.00019
Cralley JSpantidi OHoxha BFainekos G(2020)TLTk: A Toolbox for Parallel Robustness Computation of Temporal Logic SpecificationsRuntime Verification10.1007/978-3-030-60508-7_22(404-416)Online publication date: 6-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-60508-7_22

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents