Abstract
We show examples of robust systems that we have synthesized with this method by our synthesis tool {\sc Party}.
| Original language | English |
|---|---|
| Title of host publication | 2019 Formal Methods in Computer Aided Design, FMCAD 2019 |
| Editors | Clark Barrett, Jin Yang |
| Publisher | IEEE CS |
| Number of pages | 5 |
| Publication status | Accepted/In press - 2019 |
| Event | FMCAD 2019: Foraml Methods in Computer-Aided Design - San Jose, United States Duration: 22 Oct 2019 → 25 Oct 2019 |
Conference
| Conference | FMCAD 2019 |
|---|---|
| Country | United States |
| City | San Jose |
| Period | 22/10/19 → 25/10/19 |
Fingerprint
Cite this
Synthesizing Reactive Systems Using Robustness and Recovery Specifications. / Bloem, Roderick; Chockler, Hana; Ebrahimi, Masoud; Strichman, Ofer.
2019 Formal Methods in Computer Aided Design, FMCAD 2019. ed. / Clark Barrett; Jin Yang. IEEE CS, 2019.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
}
TY - GEN
T1 - Synthesizing Reactive Systems Using Robustness and Recovery Specifications
AU - Bloem, Roderick
AU - Chockler, Hana
AU - Ebrahimi, Masoud
AU - Strichman, Ofer
PY - 2019
Y1 - 2019
N2 - Past literature on synthesis identified the need to synthesize systems that are \emph{robust} to failures of the system in reading the inputs from the environment, and also to failures of the environment itself to satisfy our assumptions about its behavior. In this work, we propose a simple and flexible framework for synthesizing robust systems, where the user defines the required robustness via a temporal \emph{robustness specification}. For example, the user may specify that the environment is \emph{eventually} reliable, or input misreadings cannot occur more than $k$ consecutive steps, and synthesize a system under this assumption. Furthermore, our framework enables us to specify, also, a temporal \emph{recovery specification}, i.e., describing the way the system is expected to recover after a failure of the environment assumptions. We show examples of robust systems that we have synthesized with this method by our synthesis tool {\sc Party}.
AB - Past literature on synthesis identified the need to synthesize systems that are \emph{robust} to failures of the system in reading the inputs from the environment, and also to failures of the environment itself to satisfy our assumptions about its behavior. In this work, we propose a simple and flexible framework for synthesizing robust systems, where the user defines the required robustness via a temporal \emph{robustness specification}. For example, the user may specify that the environment is \emph{eventually} reliable, or input misreadings cannot occur more than $k$ consecutive steps, and synthesize a system under this assumption. Furthermore, our framework enables us to specify, also, a temporal \emph{recovery specification}, i.e., describing the way the system is expected to recover after a failure of the environment assumptions. We show examples of robust systems that we have synthesized with this method by our synthesis tool {\sc Party}.
M3 - Conference contribution
BT - 2019 Formal Methods in Computer Aided Design, FMCAD 2019
A2 - Barrett, Clark
A2 - Yang, Jin
PB - IEEE CS
ER -