Visible to the public DryVR 2.0: A Tool for Verification and Controller Synthesis of Black-box Cyber-physical Systems

TitleDryVR 2.0: A Tool for Verification and Controller Synthesis of Black-box Cyber-physical Systems
Publication TypeConference Paper
Year of Publication2018
AuthorsQi, Bolun, Fan, Chuchu, Jiang, Minghao, Mitra, Sayan
Conference NameProceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week)
PublisherACM
Conference LocationNew York, NY, USA
ISBN Number978-1-4503-5642-8
Keywordscomposability, Metrics, pubcrawl, resilience, White Box Security
AbstractWe 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.
URLhttp://doi.acm.org/10.1145/3178126.3187008
DOI10.1145/3178126.3187008
Citation Keyqi_dryvr_2018