Synthesizing Runtime Enforcer of Safety Properties Under Burst Error
We propose a game-based method for synthesizing a runtime enforcer for a reactive system to ensure that a set of safety-critical properties always holds even if errors occur in the system due to design defect or environmental disturbance. The runtime enfo
- PDF / 1,126,961 Bytes
- 17 Pages / 439.37 x 666.142 pts Page_size
- 104 Downloads / 133 Views
Abstract. We propose a game-based method for synthesizing a runtime enforcer for a reactive system to ensure that a set of safety-critical properties always holds even if errors occur in the system due to design defect or environmental disturbance. The runtime enforcer does not modify the internals of the system or provide a redundant implementation; instead, it monitors the input and output of the system and corrects any erroneous output signal that may cause a safety violation. Our main contribution is a new algorithm for synthesizing a runtime enforcer that can respond to violations instantaneously and guarantee the safety of the system under burst error. This is in contrast to existing methods that either require significant delay before the enforcer can respond to violations or do not handle burst error. We have implemented our method in a synthesis tool and evaluated it on a set of temporal logic specifications. Our experiments show that the enforcer synthesized by our method can robustly handle a wide range of properties under burst error.
1
Introduction
A reactive system is a system that continuously responds to external events. In practice, reactive systems may have strict timing requirements that demand them to respond without any delay. Furthermore, they are often safety-critical in that a violation may lead to catastrophe. In this context, it is important to guarantee with certainty that the system satisfies a small set of safety properties even in the presence of design defect and environmental disturbance. However, traditional verification and fault-tolerance techniques cannot accomplish this task. In particular, fault-tolerance techniques are not effective in dealing with design defects whereas verification techniques are not effective in dealing with transient faults introduced by the environment. Furthermore, formal verification techniques such as model checking are limited in handling large designs and third-party IP cores without the source code. In this paper, we propose a new method for synthesizing a runtime enforcer to make sure that a set of safety-critical properties are always satisfied even if the original reactive system occasionally makes mistakes. Unlike the replica in faulttolerance techniques, our runtime enforcer is significantly cheaper in that it does not attempt to duplicate the functionality of the original system. Instead, it aims at preventing the violation of only a handful of safety properties whose violations c Springer International Publishing Switzerland 2016 S. Rayadurgam and O. Tkachuk (Eds.): NFM 2016, LNCS 9690, pp. 65–81, 2016. DOI: 10.1007/978-3-319-40648-0 6
66
M. Wu et al.
may lead to catastrophe. Our approach also differs from classic methods for synthesizing a reactive system itself from the complete specification [14], which is known to be computationally expensive. In our approach, for example, it is perfectly acceptable for the system to violate some liveness properties, e.g., something good may never happen, as long as it guarantees that safety-critical viola
Data Loading...
