demonstration

DryVR 2.0: A tool for verification and controller synthesis of black-box cyber-physical systems

Authors:

Bolun Qi,

Chuchu Fan,

Minghao Jiang,

Sayan MitraAuthors Info & Claims

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Pages 269 - 270

https://doi.org/10.1145/3178126.3187008

Published: 11 April 2018 Publication History

Get Access

Abstract

We present a demo of DryVR 2.0, a framework for verification and controller synthesis of cyber-physical systems composed of black-box simulators and white-box automata. For verification, DryVR 2.0 takes as input a black-box simulator, a white-box transition graph, a time bound and a safety specification. As output it generates over-approximations of the reachable states and returns "Safe" if the system meets the given bounded safety specification, or it returns "Unsafe" with a counter-example. For controller synthesis, DryVR 2.0 takes as input black-box simulator(s) and a reach-avoid specification, and uses RRTs to find a transition graph such that the combined system satisfies the given specification.

References

[1]

Nicole Chan and Sayan Mitra. 2017. Verified hybrid LQ control for autonomous spacecraft rendezvous. In CDC.

Google Scholar

[2]

Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In cav. Springer, 258--263.

Google Scholar

[3]

Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan, and Matthew Potok. 2015. C2E2: A Verification Tool for Stateflow Models. In tacas. 68--82.

Digital Library

Google Scholar

[4]

Chuchu Fan, Bolun Qi, Sayan Mitra, and Mahesh Viswanathan. 2017. DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems. In CAV, Part I. 441--461.

Google Scholar

[5]

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 CAV. Springer, 379--395.

Digital Library

Google Scholar

[6]

Xiaoqing Jin, Jyotirmoy V Deshmukh, James Kapinski, Koichi Ueda, and Ken Butts. 2014. Powertrain control verification benchmark. In hscc. ACM, 253--262.

Digital Library

Google Scholar

[7]

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

Google Scholar

Cited By

View all

Yancosek JBaheri A(2024)BEACON: A Bayesian Evolutionary Approach for Counterexample Generation of Control SystemsIEEE Access10.1109/ACCESS.2024.343651512(106455-106465)Online publication date: 2024
Fan C(2024)Formal Methods for Safe AutonomyundefinedOnline publication date: 11-Oct-2024
Devonport AYang FGhaoui LArcak M(2023)Data-Driven Reachability and Support Estimation With Christoffel FunctionsIEEE Transactions on Automatic Control10.1109/TAC.2023.328174968:9(5216-5229)Online publication date: Sep-2023
Show More Cited By

Recommendations

Cascade 2.0
VMCAI 2014: Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8318

Cascade is a program static analysis tool developed at New York University. Cascade takes as input a program and a control file. The control file specifies one or more assertions to be checked together with restrictions on program behaviors. The tool ...
Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems
MEMOCODE '08: Proceedings of the Sixth ACM/IEEE International Conference on Formal Methods and Models for Co-Design

Equivalence checking is a classical verification method determining if a finite-state concurrent system (protocol) satisfies its desired external behaviour (service) by comparing their underlying labeled transition systems (LTSs) modulo an appropriate ...
DiVinE 2.0: High-Performance Model Checking
HIBI '09: Proceedings of the 2009 International Workshop on High Performance Computational Systems Biology

We present a tool for parallel enumerative LTL model-checking andreachability analysis. The tool brings model checking to high-poweredmulti-core systems, as well as high-performance clusters. Boasting pluggablemodelling language framework, it is ...

Comments

Information & Contributors

Information

Published In

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

April 2018

296 pages

ISBN:9781450356428

DOI:10.1145/3178126

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Check for updates

Qualifiers

Demonstration
Research
Refereed limited

Conference

HSCC '18

Sponsor:

SIGBED

HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control

April 11 - 13, 2018

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
171
Total Downloads

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

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Yancosek JBaheri A(2024)BEACON: A Bayesian Evolutionary Approach for Counterexample Generation of Control SystemsIEEE Access10.1109/ACCESS.2024.343651512(106455-106465)Online publication date: 2024
Fan C(2024)Formal Methods for Safe AutonomyundefinedOnline publication date: 11-Oct-2024
Devonport AYang FGhaoui LArcak M(2023)Data-Driven Reachability and Support Estimation With Christoffel FunctionsIEEE Transactions on Automatic Control10.1109/TAC.2023.328174968:9(5216-5229)Online publication date: Sep-2023
Devonport AArcak M(2023)Data-Driven Estimation of Forward Reachable SetsComputation-Aware Algorithmic Design for Cyber-Physical Systems10.1007/978-3-031-43448-8_8(165-185)Online publication date: 25-Aug-2023
Baheri A(2023)Exploring the role of simulator fidelity in the safety validation of learning‐enabled autonomous systemsAI Magazine10.1002/aaai.12141Online publication date: 27-Nov-2023
Devonport AYang FEl Ghaoui LArcak M(2021)Data-Driven Reachability Analysis with Christoffel Functions2021 60th IEEE Conference on Decision and Control (CDC)10.1109/CDC45484.2021.9682860(5067-5072)Online publication date: 14-Dec-2021
Malladi BSanfelice RButcher E(2021)Robust hybrid supervisory control for spacecraft close proximity missionsAnnual Reviews in Control10.1016/j.arcontrol.2021.11.00152(316-329)Online publication date: 2021

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.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Recommendations

Cascade 2.0

Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems

DiVinE 2.0: High-Performance Model Checking

Comments

Information

Published In

Sponsors

Publisher

Publication History

Check for updates

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations