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

Bolun Qi; Chuchu Fan; Minghao Jiang; Sayan Mitra

doi:10.1145/3178126.3187008

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

Bolun Qi, Chuchu Fan, Minghao Jiang, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English (US)
Title of host publication	HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems
Subtitle of host publication	Computation and Control (part of CPS Week)
Publisher	Association for Computing Machinery, Inc
Pages	269-270
Number of pages	2
ISBN (Electronic)	9781450356428
DOIs	https://doi.org/10.1145/3178126.3187008
State	Published - Apr 11 2018
Event	21st International Conference on Hybrid Systems: Computation and Control, HSCC 2018 - Porto, Portugal Duration: Apr 11 2018 → Apr 13 2018

Publication series

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

Other

Other	21st International Conference on Hybrid Systems: Computation and Control, HSCC 2018
Country	Portugal
City	Porto
Period	4/11/18 → 4/13/18

ASJC Scopus subject areas

Computer Science Applications
Electrical and Electronic Engineering
Control and Systems Engineering
Computer Networks and Communications

Access to Document

10.1145/3178126.3187008

Fingerprint Dive into the research topics of 'Demo: DryVR 2.0 - A tool for verification and controller synthesis of black-box cyber-physical systems'. Together they form a unique fingerprint.

Cite this

Qi, B., Fan, C., Jiang, M., & Mitra, S. (2018). Demo: DryVR 2.0 - A tool for verification and controller synthesis of black-box cyber-physical systems. In HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week) (pp. 269-270). (HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)). Association for Computing Machinery, Inc. https://doi.org/10.1145/3178126.3187008

Demo : DryVR 2.0 - A tool for verification and controller synthesis of black-box cyber-physical systems. / Qi, Bolun; Fan, Chuchu; Jiang, Minghao; Mitra, Sayan.

HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week). Association for Computing Machinery, Inc, 2018. p. 269-270 (HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Qi, B, Fan, C, Jiang, M & Mitra, S 2018, Demo: DryVR 2.0 - A tool for verification and controller synthesis of black-box cyber-physical systems. in HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week). HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), Association for Computing Machinery, Inc, pp. 269-270, 21st International Conference on Hybrid Systems: Computation and Control, HSCC 2018, Porto, Portugal, 4/11/18. https://doi.org/10.1145/3178126.3187008

Qi B, Fan C, Jiang M, Mitra S. Demo: DryVR 2.0 - A tool for verification and controller synthesis of black-box cyber-physical systems. In HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week). Association for Computing Machinery, Inc. 2018. p. 269-270. (HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)). https://doi.org/10.1145/3178126.3187008

Qi, Bolun ; Fan, Chuchu ; Jiang, Minghao ; Mitra, Sayan. / Demo : DryVR 2.0 - A tool for verification and controller synthesis of black-box cyber-physical systems. HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week). Association for Computing Machinery, Inc, 2018. pp. 269-270 (HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)).

@inproceedings{cedc87c5926141bba6c7c09623ad45f6,

title = "Demo: DryVR 2.0 - A tool for verification and controller synthesis of black-box cyber-physical systems",

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.",

author = "Bolun Qi and Chuchu Fan and Minghao Jiang and Sayan Mitra",

note = "Funding Information: This work is supported by National Science Foundation's research grants NSF CAREER 1054247 and NSF CSR 1422798.; 21st International Conference on Hybrid Systems: Computation and Control, HSCC 2018 ; Conference date: 11-04-2018 Through 13-04-2018",

year = "2018",

month = apr,

day = "11",

doi = "10.1145/3178126.3187008",

language = "English (US)",

series = "HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)",

publisher = "Association for Computing Machinery, Inc",

pages = "269--270",

booktitle = "HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems",

}

TY - GEN

T1 - Demo

T2 - 21st International Conference on Hybrid Systems: Computation and Control, HSCC 2018

AU - Qi, Bolun

AU - Fan, Chuchu

AU - Jiang, Minghao

AU - Mitra, Sayan

N1 - Funding Information: This work is supported by National Science Foundation's research grants NSF CAREER 1054247 and NSF CSR 1422798.

PY - 2018/4/11

Y1 - 2018/4/11

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85049448453&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85049448453&partnerID=8YFLogxK

U2 - 10.1145/3178126.3187008

DO - 10.1145/3178126.3187008

M3 - Conference contribution

AN - SCOPUS:85049448453

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

SP - 269

EP - 270

BT - HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems

PB - Association for Computing Machinery, Inc

Y2 - 11 April 2018 through 13 April 2018

ER -