Synthesizing reactive systems using robustness and recovery specifications

TY - CHAP

T1 - Synthesizing reactive systems using robustness and recovery specifications

AU - Bloem, Roderick

AU - Chockler, Hana

AU - Ebrahimi, Masoud

AU - Strichman, Ofer

PY - 2019/10/1

Y1 - 2019/10/1

N2 - Past literature on synthesis identified the need to synthesize systems that are 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 robustness specification. For example, the user may specify that the environment is 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 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 PARTY.

AB - Past literature on synthesis identified the need to synthesize systems that are 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 robustness specification. For example, the user may specify that the environment is 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 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 PARTY.

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

U2 - 10.23919/FMCAD.2019.8894276

DO - 10.23919/FMCAD.2019.8894276

M3 - Conference paper

SP - 147

EP - 151

BT - Proceedings of the 19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019

A2 - Barrett, Clark

A2 - Yang, Jin

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019

Y2 - 22 October 2019 through 25 October 2019

ER -