Title | DryVR 2.0: A Tool for Verification and Controller Synthesis of Black-box Cyber-physical Systems |
Publication Type | Conference Paper |
Year of Publication | 2018 |
Authors | Qi, Bolun, Fan, Chuchu, Jiang, Minghao, Mitra, Sayan |
Conference Name | Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week) |
Publisher | ACM |
Conference Location | New York, NY, USA |
ISBN Number | 978-1-4503-5642-8 |
Keywords | composability, Metrics, pubcrawl, resilience, White Box Security |
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. |
URL | http://doi.acm.org/10.1145/3178126.3187008 |
DOI | 10.1145/3178126.3187008 |
Citation Key | qi_dryvr_2018 |