Synthesizing Reactive Systems Using Robustness and Recovery Specifications

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

Abstract

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}.
Original languageEnglish
Title of host publication2019 Formal Methods in Computer Aided Design, FMCAD 2019
EditorsClark Barrett, Jin Yang
PublisherIEEE CS
Number of pages5
Publication statusAccepted/In press - 2019
Event FMCAD 2019: Foraml Methods in Computer-Aided Design - San Jose, United States
Duration: 22 Oct 201925 Oct 2019

Conference

Conference FMCAD 2019
CountryUnited States
CitySan Jose
Period22/10/1925/10/19

Fingerprint

Specifications
Recovery

Cite this

Bloem, R., Chockler, H., Ebrahimi, M., & Strichman, O. (Accepted/In press). Synthesizing Reactive Systems Using Robustness and Recovery Specifications. In C. Barrett, & J. Yang (Eds.), 2019 Formal Methods in Computer Aided Design, FMCAD 2019 IEEE CS.

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 proceedingConference contributionResearchpeer-review

Bloem, R, Chockler, H, Ebrahimi, M & Strichman, O 2019, Synthesizing Reactive Systems Using Robustness and Recovery Specifications. in C Barrett & J Yang (eds), 2019 Formal Methods in Computer Aided Design, FMCAD 2019. IEEE CS, FMCAD 2019, San Jose, United States, 22/10/19.
Bloem R, Chockler H, Ebrahimi M, Strichman O. Synthesizing Reactive Systems Using Robustness and Recovery Specifications. In Barrett C, Yang J, editors, 2019 Formal Methods in Computer Aided Design, FMCAD 2019. IEEE CS. 2019
Bloem, Roderick ; Chockler, Hana ; Ebrahimi, Masoud ; Strichman, Ofer. / Synthesizing Reactive Systems Using Robustness and Recovery Specifications. 2019 Formal Methods in Computer Aided Design, FMCAD 2019. editor / Clark Barrett ; Jin Yang. IEEE CS, 2019.
@inproceedings{41b3da7c9f3c4d728ac1cad401022ee5,
title = "Synthesizing Reactive Systems Using Robustness and Recovery Specifications",
abstract = "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}.",
author = "Roderick Bloem and Hana Chockler and Masoud Ebrahimi and Ofer Strichman",
year = "2019",
language = "English",
editor = "Clark Barrett and Jin Yang",
booktitle = "2019 Formal Methods in Computer Aided Design, FMCAD 2019",
publisher = "IEEE CS",

}

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 -