1 Introduction
A system with sporadic errors (SSE) is a controller which produces high quality desirable output for any given input but it may sporadically violate a critical system requirement , where I and O are the set of input and output propositions. Many manually designed controllers have this character, as they embody designer’s unspecified optimizations, however they may have obscure design errors. A runtime enforcement shield for a specified critical requirement is a controller (Mealy machine) which receives both input and output generated by SSE. The shield produces a modified output which is guaranteed to invariantly meet the critical requirement (correctbyconstruction). Moreover, in each run, the shield output must deviate from the SSE output “as little as possible”, to maintain the quality. This allows the shield to benefit from system designer’s optimizations without having to formally specify these or to handle these in the synthesis. See Figure 2.
A central issue in designing runtime enforcement shields is the underlying notion of “deviating as little as possible” from the SSE output. There are several different notions explored in the literature [3, 10, 22, 21]. In their pioneering paper, Bloem et al. [3] proposed the notion of stabilizing shield which may deviate for at most cycles continuously under suitable assumptions. If assumptions are not met the shield may deviate arbitrarily. This was proposed as a hard requirement which must be mandatorily satisfied by the shield in any behaviour. We call such constraints as hard deviation constraints. Konighofer et al [10] have proposed some variants of the stabilizing shield requirement with and without fail safe state, which are also hard deviation constraints. Specific shield synthesis algorithms have been developed for each of these constraints.
As our first main contribution, we propose a logical specification notation for hard deviation constraints using the formulas of an interval temporal logic QDDC. This logic allows us to succinctly and modularly specify regular properties [14, 12, 13]. With its counting constructs and interval based modalities, it can be used to conveniently specify both the correctness requirement as well as the hard deviation constraint .
Criticizing the inability of stabilizing shields in handling burst errors, Wu et al. [22, 21] proposed a bursterror shield which enforces the invariance of the correctness requirement, and it locally minimizes the measure of deviation between SSE output and the shield output , at each step. An algorithm for the synthesis of such shields was given. We call such a shield as locally deviation minimizing.
In this paper, as our second main contribution, we generalize the Wu technique to minimize the cumulative deviation more globally. An optimal shield which minimizes at each point the expected value of cumulative deviation in next steps of shield execution is computed. The cumulative deviation is averaged over all possible
length inputs to arrive at the optimal estimate. A well known value iteration algorithm
[2, 17]for optimal policy synthesis of Markov Decision Processes allows us to compute such a shield. We call such a shield as
optimally deviation minimizing. This is a powerful optimization and in the paper we experimentally show its significant impact on performance of the shield. It may be noted that Wu’s bursterror shield is obtained by selecting .Finally, we propose a uniform method for synthesizing a runtime enforcement shield from given logical specification and a horizon value (natural number) . The resulting shield invariantly meets the correctness requirement as well as the hard deviation constraint . Moreover, the shield is optimally deviation minimizing. The shield synthesis is carried out by using the soft requirement guided controller synthesis tool DCSynth [19]. This tool allows synthesis of optimal controllers from specified hard and soft QDDC requirements.
Using the proposed formalism, in the paper, we formulate several diverse notions of shields. These include a logical specification of Bloem’s stabilizing shield and Wu’s bursterror shield, as well as a new notion of shield. A uniform synthesis method using the tool DCSynth can be applied to obtain the corresponding runtime enforcement shields. It is notable that tool DCSynth uses an efficient BDDbased semisymbolic representation of automata/controllers with aggressive minimization. This allows the tool to scale better and to produce smaller sized shields. In the paper, we give an experimental evaluation of the performance of our DCSynth tool and compare it with some previously reported studies in the literature.
With the ability to formulate shields with diverse hard deviation constraints, it is natural to ask for a comparison of the performance of these shields. The performance must essentially measure the extent of deviation of the shield output from the SSE output. Towards this, we propose two measures of the shield performance.

We compute the probability of deviation in long run. For this, we assume that the input to the shield is fully random, with each input variable value chosen independently of the past and each other. While simplistic, this does provide some indication of the shield’s effectiveness in average.

We measure the worst case burstdeviation latency. This gives the maximum number of consecutive deviations possible in the worst case. (If unbounded, we report ). A model checking technique implemented in a tool CTLDC [15] allows us to compute this worst case latency.
Tool DCSynth provides facilities for the computation of each of these performance measures for a synthesized shield. The reader may refer to the original papers on DCSynth [19, 16] for details of techniques by which such performance can be measured. In this paper, we synthesize shields with different hard deviation constraints and we provide a comparison of the performance of these shields. This allows us to draw some preliminary conclusions. Clearly, much wider experimentation is needed for firmer insight.
The rest of the paper is organized as follows. Section 2.1 describes the syntax and semantics of the logic QDDC. Section 2.3 gives the syntax of DCSynth specification and brief outline of the synthesis method. Section 3 describes the various logical notions of shield specification. Section 4 describes metrics to evaluate the shield performance and corresponding experimental results. In Section 5, we conclude the paper with discussion and related work.
2 Preliminaries
We provide a brief overview of logic QDDC as well as the soft requirement guided optimal controller synthesis method implemented in tool DCSynth. This method and tool is applied to the problem of runtime enforcement shield synthesis in this paper. The reader may refer to the original paper [19] for further details of these preliminaries.
2.1 Quantified Discrete Duration Calculus (QDDC) Logic
Let be a finite nonempty set of propositional variables. Let a nonempty finite word over the alphabet . It has the form where for each . Let , , and .
The syntax of a propositional formula over variables is given by:
with denoting conjunction, disjunction and negation, respectively. Operators such as and are defined as usual. Let be the set of all propositional formulas over variables . Let . Then the satisfaction of propositional formula at point , denoted is defined as usual and omitted here for brevity.
The syntax of a QDDC formula over variables is given by:
where , , and .
An interval over a word is of the form where and . Let be the set of all intervals over . Let be a word over , let be an interval. Then the satisfaction of a QDDC formula written as , is defined inductively as follows:
with Boolean combinations , and defined in the expected way. We call word a variant, , of a word if . Then for some variant of ; and .
Entities , and are called terms. The term gives the length of the interval in which it is measured. Term , where , counts the number of positions including the first and the last point in the interval under consideration where holds. Formally, for we have , and .
We also define the following derived constructs: , , , and . Thus, iff for all subintervals and iff for all prefix intervals .
Finally, we define iff , and iff . Let , the set of behaviours accepted by . Let be valid, denoted , iff . Notice that denotes that the past of position satisfies the formula .
Example 1.
We give an example QDDC formula over propositions which specifies a typical recurrent reachavoid behaviour required in many control systems. Intuitively, the formula holds at a position in the behaviour if, since the previous occurrence of , the proposition persists till an occurrence of . Moreover, must occur within time units from the last occurrence of . For example, here may denote entering of enemy airspace, may denote that the UAV is invisible and may denote that the target is reached. Let abbreviate . Figure 1 gives a possible behaviour where the last row gives the value of for each position .

:
((slen<(n)) && [[p]])
(((([p]
pt)^<q>) && slen<=n)^true)
.
The second disjunct holds for an interval provided occurs at a position with and persists from to . E.g. in Figure 1, with . The first disjunct holds for an interval provided and holds throughout the interval. E.g. . Note that . 
:
!(true^(<p>^((slen=1^[[!p]])
pt) && !(D)))
This formula fails to hold at position provided there is a previous (last) occurrence of in the past of , at say position , and does not hold for the interval . 
Let be the QDDC formula
SinceLast(r,(Until(p,q,n)))
.Then, since there is no at any position . Also, as, since the previous occurrence of at position , the proposition persists till and holds at (with ). Note also that since the previous occurs at (with ) and . Finally, as, since the previous at position , neither does occur inbetween nor do we have . ∎
Theorem 2.
[14] For every formula over variables we can construct a Deterministic Finite Automaton (DFA) over alphabet such that . We call a formula automaton for or the monitor automaton for . ∎
A tool DCVALID implements this formula automaton construction in an efficient manner by internally using the tool MONA [9]. It gives minimal, deterministic automaton (DFA) for the formula . We omit the details here. However, the reader may refer to several papers on QDDC for detailed description and examples of QDDC specifications as well as its model checking tool DCVALID [14, 12, 13].
In the rest of the paper we consider QDDC formulas and automata where variables are partitioned into disjoint sets of input variables and output variables . Such a formula/automaton specifies a relation between inputs and outputs.
For technical convenience, we define a notion of indicator variable for a QDDC formula (regular property). The idea is that the indicator variable witnesses the truth of a formula at any point in execution. Thus, . Here, , i.e. in a behaviour and a position , we have iff . If then for for any , we have iff . Thus variable is true exactly at those positions where the past of the position satisfies . These indicator variables can be used as auxiliary propositions in another formula using the notion of cascade composition defined below.
Definition 3 (Cascade Composition).
Let be QDDC formulas over inputoutput variables and let be the corresponding set of fresh indicator variables i.e. . Let be a formula over variables . Then, the cascade composition and its equivalent QDDC formula are as follows:
This composition gives a formula over inputoutput variables . ∎
Cascade composition provides a useful ability to modularize a formula using auxiliary propositions which witness other regular properties given as QDDC formulas.
Example 4.
Consider a formula ) which holds at a point provided the proposition is at most 3 times in the entire past. Let formula which holds at a point provided that the values of propositions o
and o’
differ at that position. Then, is equivalent to the formula . This formula holds at a position i
, provided D1
holds at most time in the interval [0,i]
. That is o
o’
for atmost positions in the interval [0,i]
. ∎
2.2 Supervisors and Controllers
Now we consider QDDC formulas and automata where variables are partitioned into disjoint sets of input variables and output variables . We show how Mealy machines can be represented as special form of Deterministic finite automata (DFA). Supervisors and controllers are Mealy machines with special properties. This representation allows us to use the MONA DFA library [9] to efficiently compute supervisors and controllers in our tool DCSynth.
Definition 5 (Outputnondeterministic Mealy Machines).
A total and Deterministic Finite Automaton (DFA) over inputoutput alphabet is a tuple , as usual, with . An outputnondeterministic Mealy machine is a DFA with a unique reject (or nonfinal) state which is a sink state i.e. and for all , . ∎
Intuition is that the transitions from to are forbidden (and kept only for making the DFA total). Language of any such Mealy machine is prefixclosed. Recall that for a Mealy machine, . A Mealy machine is deterministic if , , at most one s.t. . An outputnondeterministic Mealy machine is called nonblocking if , s.t. . It follows that for all input sequences a nonblocking Mealy machine can produce one or more output sequence without ever getting into the reject state.
For a Mealy machine over variables , its language . A word can also be represented as pair such that . Here must have the same length. We will not distinguish between and in the rest of the paper. Also, for any input sequence , we will define .
Definition 6 (Controllers and Supervisors).
An outputnondeterministic Mealy machine which is nonblocking is called a supervisor. A deterministic supervisor is called a controller. ∎
The nondeterministic choice of outputs in a supervisor denotes unresolved decision. The determinism ordering below allows supervisors to be refined into controllers.
Definition 7 (Determinism Order and Subsupervisor).
Given two supervisors we say that is more deterministic than , denoted , iff . We call to be a subsupervisor of . ∎
Note that being supervisors, they are both nonblocking, and hence for any . The supervisor may make use of additional memory for resolving and pruning the nondeterminism in .
2.3 DCSynth Specification and Controller Synthesis
This section gives a brief overview of the soft requirement guided controller synthesis method from QDDC formulas. The method is implemented in a tool DCSynth. (See [19] for details). This method and the tool will be used for synthesis of runtime enforcement shields in the subsequent sections.
Definition 8.
A supervisor realizes invariance of QDDC formula over variables , denoted as , provided . Recall that, by the definition of supervisors, must be nonblocking. The supervisor is called maximally permissive provided for any supervisor such that , we have . Thus, no other supervisor with larger languages realizes the invariance of . This is unique up to language equivalence of automata, and the minimum state maximally permissive supervisor is denoted by . ∎
A wellknown greatest fixed point algorithm for safety synthesis over gives us if it is realizable. We omit the details here (see [19]).
Proposition 9 (MPS Monotonicity).
Given QDDC formulas and over variables such that , we have:

, and

If is realizable then is also realizable. ∎
A DCSynth specification is a tuple where and are the set of input and output variables, respectively. Formula , called the hard requirement, and formula , called the soft requirement, are QDDC formulas over the set of propositions . The objective in DCSynth is to synthesize a deterministic controller which (a) invariantly satisfies the hard requirement , and (b) optimally satisfies for as many inputs as possible.
The controller synthesis goes through following three stages.

The DCSynth specification is said to be realizable iff is realizable (i.e. it exist). The synthesis method first computes the maximally permissive supervisor realizing invariance of . When clear from context we will abbreviate this as .

A subsupervisor of which satisfies for “as many inputs as possible” is computed. This is formalized using a notion of optimality w.r.t. the soft requirement . We explain this only intuitively. The reader may refer to the original paper [19] for a formal definition of optimality and the synthesis algorithm. Let be a natural number called horizon. We construct the maximally permissive subsupervisor of , called , by pruning the nondeterministic choice of outputs in and retaining only the outputs which give the highest expected count of (intermittent) occurrence of over the next steps of execution. This count is averaged over all input sequences of length . A well known valueiteration algorithm due to Bellman [2], adapted from optimal strategy synthesis for Markov Decision Processes [17], gives us the required optimal maximally permissive subsupervisor. See the paper [19] for full details which are omitted here. Note that, by construction, . By Definition 7, all the behaviours of will invariantly satisfy and the will be optimal with respect to . When clear from context, will be abbreviated as .

Both and are supervisors and they may be outputnondeterministic as there can be several optimal outputs possible. Any controller obtained by arbitrarily resolving the output nondeterminism in will also be optimal. In tool DCSynth, we allow users to specify a preference ordering on the set of outputs . Any supervisor can be determinized by retaining only the highest ordered output among those permitted by . This is denoted by . In tool DCSynth, the output ordering is specified by giving a lexicographically ordered list of output variable literals, as illustrated in Example 10 below. This facility is used to determinize supervisors and as required. These are denoted by and .
Example 10.
For a supervisor over variables , an output ordering can be given as list (), Then, the determinization step will select the highest allowed output from the list (), (), (), () in that order. This choice is made for each state and each input. ∎
In summary, given a DCSynth specification , a horizon value and a preference ordering on outputs , the tool DCSynth outputs maximally permissive supervisors and as well as controllers and .
Extended DCSynth specification:
DCSynth supports the specification of soft requirements as an ordered list of formulas with user defined weights. This feature is used in the synthesis of runtime enforcement shields. The extended DCSynth specification is a tuple where and are sets of input and output variables respectively. The QDDC formula , which is over , specifies the hard requirement on the controller to be synthesized. The soft requirement is a list where each is a QDDC formula over . specifies the weight of the soft requirement . The weight (reward) of a transition is sum of weights of each of the formula which holds on taking the transition. The tool DCSynth produces a supervisor, which maximizes the cumulative expected value of this reward over next steps of execution. This cumulative reward is averaged over all input sequences of length .
3 Specification and Synthesis of Runtime Enforcement Shields
Given a correctness requirement as a QDDC formula over inputoutput propositions , a system with sporadic errors (SSE) may fail to meet the requirement at some of the points in a behaviour . (The reader may recall Definition 5 and its following two paragraphs for the notation.) A runtime enforcement shield is a Mealy machine with input variables and output variable . See Figure 2. For any input the shield produces a modified output such that invariantly satisfies the correctness requirement . Moreover, the output must deviate from the SSE output as little as possible to maintain quality. There are several distinct notions of “deviating as little as possible” leading to different shields.
In this section, we give a logical framework for specifying various shields by using the logic QDDC. We then provide an automatic synthesis of a runtime enforcement shield from its logical specification using the tool DCSynth of the previous section. Thus, we achieve a logical specification and a uniform synthesis method for shields.
Deviation constraints specify the extent of allowed deviation in a shield’s behaviour. Our specification has hard deviation constraint which must be mandatorily and invariantly satisfied by the shield. (This is similar to the hard requirement in DCSynth.) We also define a canonical soft deviation constraint which will be useful in minimizing cumulative deviation during synthesis. Overall, a shield specification consists of a pair .
3.1 Hard Deviation Constraints
Two indicator propositions, and play an important role in formulating hard deviation constraints. Proposition indicates whether the SSE is meeting the requirement at the current position. Proposition indicates whether at the current position, the shield output is different from the SSE output. Recall that in DCSynth specifications, the formula defines a fresh output proposition which is true at a position provided the past of the position satisfies formula (see Definition 3). We use the following list of indicator definitions in formulating hard deviation constraints. Let, and .
A hard deviation constraint is a QDDC formula over propositions and . It specifies a constraint on conditional upon the behaviour of . In Subsection 3.4, we will give a list of several different hard deviation constraints.
For shield synthesis using DCSynth, we define the QDDC formula given in Equation 1) as the hard requirement over the inputoutput propositions . Notice that in its formulation, we use the cascade composition from Definition 3. This allows us to modularize the specification into components and .
(1) 
The constraint (QDDC formula) must be invariantly satisfied by the shield. Tool DCSynth gives us a maximally permissive supervisor with this property (See definition 8). This supervisor can be termed as shieldsupervisor without deviation minimization and it will be denoted by .
3.2 Soft Deviation Constraint
While already places some constraints on the permitted deviation, we can further optimize the deviation in supervisor of the previous section. Quantitative optimization techniques from Markov Decision Processes can be used. (Stocasticity comes from the distribution of inputs to the shield.) The tool DCSynth allows us to specify such optimization using a list of soft requirement formulas with weights. The tool optimizes a supervisor to a subsupervisor which maximizes the expected value of cumulative weight of soft requirements over next steps. This cumulative weight is averaged over all input sequences of length . See Section 2.3 and [19] for further details.
We make use of this optimal subsupervisor computation to get a subsupervisor which minimizes the expected cumulative deviation over next steps. Given the set of output propositions , consider the DCSynth softrequirement
(2) 
Thus, nondeviation of any output variable at current position contributes a reward . This is summed over all output variables to give weight (reward) of the soft requirement. Thus, the weight of the soft requirement at any position in a word is the value where is the hamming distance between and . If and perfectly match at position then the weight at position is , whereas if and differ in values of say variables at position then the weight at the position is .
By using as soft requirement and by selecting a horizon value , we can apply the tool DCSynth to obtain a subsupervisor
of the supervisor . This subsupervisor retains only the outputs which maximize the expected accumulated weight of over next steps in future. This supervisor is called the shieldsupervisor with deviation minimization and denoted by .
3.3 Determinization
The reader must note that both the shieldsupervisors and are output nondeterministic. Multiple choice of outputs may satisfy the hard deviation constraints while being optimal for the soft deviation constraint. Any arbitrary resolution of the output nondeterminism will preserve the invariance guarantees and optimality (see [19]).
In our method, we allow the user to specify a preference ordering on the shield outputs . A lexicographically ordered list of output literals is given as explained in Example 10. A deterministic controller is obtained by retaining only the highest ordered output from the nondeterministic choice of outputs offered by the supervisor. Thus, given a preference ordering we can obtain shields (deterministic controllers) and .
In summary, given a correctness requirement to be enforced by the shield, a hard deviation constraint , a horizon value (for globally minimizing the deviation over next steps) and a preference ordering on shield outputs , we can synthesize shields and . When are clear from context, these shields are referred to as (shield with no deviation minimization) and (shield with deviation minimization), respectively.
3.4 Variety of Hard Deviation Constraints and ShieldTypes
In Table 1 below, we give a useful list of several different hard deviation constraints () as QDDC formulas. These include the specifications of the bursterror shield of Wu et al. and the stabilizing shield of Bloem et al. as well as a new notion of shield. Labels to are used to identify these specifications in the experiments. Each of these can be used to synthesize shields with or without deviation minimization as explained in the previous subsection.
ShieldType  HDC  
Burstshield  
shield  []([[Deviation]]=>slen<k) 

stabilizing shield  []([[SSEOK && Deviation]]=>slen<k) && 

( []( (<!Deviation>^[[SSEOK]]) => [[!Deviation]] ) ) 


shield  []((scount !SSEOK <= e) => (scount Deviation <=d) && 
( []( (<!Deviation>^[[SSEOK]]) => [[!Deviation]] ) ) 
We provide some explanation and comments on these specifications.

The proposition denotes that the is not making correctness error where as proposition denotes that the shield is deviating from the output. The QDDC formula
( []( (<!Deviation>^[[SSEOK]]) => [[!Deviation]] ) )
states that in any observation interval, if the interval begins with no deviation, and there is no error by SSE during the interval, then there is no deviation throughout the interval. This property can be called . It is included as a conjunct in Shield as well as Shield . 
Burstshield () does not enforce any hard deviation constraint. Thus, only hard requirement on the synthesized shield is to meet invariantly. However, we can use this together with deviation minimization using the soft deviation constraint . By taking horizon , we obtain the burst sheild of Wu et al. [22] which locally optimizes deviation at each step without any lookahead into the future. Larger horizon values give superior shields which improve the probability of nondeviation in long run, as shown by our experiments which are reported later in this paper.

A shield () specifies (as its hard deviation constraint) that for any observation interval the deviation can invariantly happen for at most cycles. Thus, a burst of deviation has length of at most cycles. The shield () specifies that this property must hold unconditionally. Such a specification is often unrealizable. For example, if SSE makes consecutive errors for more than cycles, the shield may be forced to deviate for all of these cycles. Hence, several variants of the shield have been considered.

The stabilizing shield () specifies that the shield may deviate as long as makes errors (even burst errors). Once recovers from deviation (indicated by becoming and remaining true), the shield may deviate for at most cycles. Thus, the shield must recover from deviation within cycles once is established and maintained. Also, there must be no spurious deviation due to conjunct . This specification precisely gives the stabilizing shield without failsafe state, originally defined by Konighofer et al. [10]. By a variation of this, the stabilizing shield with failsafe state [10] can also be specified but we omit this here.

We define a new notion of shield called shield (). This states that in any observation interval if the count of errors by SSE (given by the term
(scount !SSEOK)
) is at most then the count of number of cycles with deviations (given by the term(scount Deviation)
) is at most . Thus errors lead to at most deviations. Also, there is no spurious deviation due to the conjunct .
It may be noted that irrespective of the shield type the synthesized shield have to meet the requirement invariantly as specified by the formula (See Equation 1).
Specification  Stabilizing shield  Bursterror shield  Burst shield with DM  
For H=0  For H=10  
states  time  states  time  states  time  states  time  
Toyota Powertrain  38  0.2  38  0.3  9  0.07  9  0.35 
Traffic light  7  0.1  7  0.2  4  0.008  4  0.059 
67  0.7  67  0.5  67  0.009  67  0.029  
259  46.9  259  10.5  259  0.08  259  0.09  
515  509.1  515  54.4  515  0.24  515  0.26  
G( q) (q )  67  0.8  67  0.6  67  0.015  67  0.06 
G( q) (q )  259  46.2  259  10.7  259  0.16  259  0.27 
G( q) (q )  515  571.7  515  54.5  515  0.77  515  0.91 
G(q r ( r (p r)))  15  0.1  145  0.1  6  0.002  6  0.013 
G(q r ( r (p r)))  109  0.2  5519  4.5  10  0.003  10  0.023 
G(q r ( r (p r)))  753  6.3  27338  1414.5  14  0.009  14  0.03 
AMBA G1+2+3  22  0.1  22  0.1  7  0.002  7  0.01 
AMBA G1+2+4  61  6.3  78  2.2  8  0.2  8  1.69 
AMBA G1+3+4  231  55.6  640  97.6  14  0.25  14  2.01 
AMBA G1+2+3+5  370  191.8  1405  61.8  12  0.017  13  0.105 
AMBA G1+2+4+5  101  3992.9  253  472.9  12  1.27  12  8.86 
AMBA G4+5+6  252  117.9  205  26.4  18  0.86  18  7.99 
AMBA G5+6+10  329  9.8  396  31.4  27  3.7  27  36.14 
AMBA G5+6+9e4+10  455  17.6  804  42.1  46  5.58  46  52.96 
AMBA G5+6+9e8+10  739  34.9  1349  86.8  64  7.44  64  70.73 
AMBA G5+6+9e16+10  1293  74.7  2420  189.7  100  11.3  100  105.2 
AMBA G5+6+9e64+10  4648  1080.8  9174  2182.5  316  37.17  316  202.52 
AMBA G8+9e4+10  204  7.0  254  6.1  48  0.29  16  2.13 
AMBA G8+9e8+10  422  22.5  685  33.7  84  0.55  20  3.49 
AMBA G8+9e16+10  830  83.7  1736  103.1  156  1.02  28  6.32 
AMBA G8+9e64+10  3278  2274.2  7859  2271.5  588  5.96  76  24.89 
4 Performance Measurement Metrics and Experiments
In this section we give the experimental results for shield synthesis carried out in our framework. We first benchmark the performance of our tool and compare it with some other tools for shield synthesis in Section 4.1. In Section 4.2 we define some performance measurement metrics for shields and we use these to compare various shield types.
4.1 Performance of Tool DCSynth in Shield Synthesis
We have synthesized Burstshield with deviation minimization using DCSynth for all the benchmark examples given in [22]. The results are tabulated in Table 2. All our experiments were conducted on Linux (Ubuntu 18.04) system with Intel i5 64 bit, 2.5 GHz processor and 4 GB memory. The formula automata files of Wu et al.[20] were used in place of QDDC formulas for uniformity. For a comparision with other tools, the results for the stabilizing shield synthesis and the Bursterror shield synthesis for the same examples are reproduced directly from Wu et al. [22]. As these are for unknown hardware setup, a direct comparison of the synthesis times with the DCSynth synthesis times is only indicative.
As the table suggests, in most of the cases, the shield synthesized by DCSynth compares favorably with the results reported in literature [22], both in terms of the size of the shield and the time taken for the synthesis. Recall that DCSynth uses aggressive minimization to obtain smaller shields. As an example, for the specification AMBA G5+6+9e64+10, our tool synthesizes a shield significantly faster and with smaller number of states than the existing tools[3, 22].
4.2 Comparison between various shield notions
For comparing the performance of shields synthesized with different shield types, we define the following performance metrics.
Expected Value of Nondeviation of a Shield in Long run:
A shield is said to be in a nondeviating state if the shield output matches the SSE output . A proposition !Deviation
holds for such states.
We measure the probability of shield being in such states over its long runs, as described below.
Given a shield over inputoutput propositions and a QDDC formula (regular property) over variables , we construct a
Discrete Time Markov Chain (DTMC)
, denoted as , whose analysis allows us to measure the probability of holding in long runs (steady state) of under independent and identically distributed (iid) inputs. This value is called the expected value of holding in a shield and designated as .The construction of the desired DTMC is as follows. The product gives a finite state automaton with the same behaviours as . Moreover, it is in accepting state exactly when holds for the past behaviour. (Here works as a total deterministic monitor automaton for without restricting ). By assigning uniform discrete probabilities to all the inputs from any state, we obtain the DTMC along with a designated set of accepting states. The DTMC is in accepting state precisely when holds. Standard techniques from Markov chain analysis allow us to compute the probability (Expected value) of being in the set of accepting states on long runs (steady state) of the DTMC. This gives us the desired value . A leading probabilistic model checking tool MRMC implements this computation [8]. In DCSynth, we provide a facility to compute in a format accepted by the tool MRMC. Hence, using DCSynth and MRMC, we are able to compute .
The expected value of a shield being in a nondeviating state over long runs can be computed as true^<!Deviation>
.
Worst Case BurstDeviation Latency:
The worst case burstdeviation latency gives the maximum number of consecutive cycles for which the shield deviates even when the SSE is satisfying the requirement. Thus, it denotes the maximum length of an interval in the behaviour of the shield for which the formula “” holds invariantly.
Given a Shield and a QDDC formula , the latency goal computes
i. e. it computes the length of the longest interval satisfying across all the executions of . Thus, it computes the worst case span of behaviour fragments matching in . Tool CTLDC [15] implements a model checking technique for computing MAXLEN(D,S). The worst case burst deviation latency of shield measures the maximum number of consecutive cycles having deviation in worst case. The worst case burstdeviation latency of a shield can be computed as .
Sr. No.  Shield Type  States  Time  Expected Value  Latency 
Shield Synthesis of Requirement Without Deviation Minimization  
1.  _NoDM  18  0.004  0.25  
2.  _NoDM(k=1)  Unrealizable  
3.  _NoDM(k=1)  14  0.004  0.7142793  1 
4.  _NoDM(k=3)  Unrealizable  
5.  _NoDM(k=3)  18  0.009  0.5982051  3 
6.  _NoDM(e=1,d=1)  13  0.001  0.7499943  0 
7.  _NoDM(e=1,d=2)  26  0.005  0.7182475  1 
8.  _NoDM(e=1,d=3)  40  0.008  0.6614611  2 
Shield Synthesis of Requirement With Deviation Minimization 

9.  _DM(k=1)  Unrealizable  
10.  _DM(H=0)  13  0.003  0.833252  0 
11.  _DM(k=1)(H=0)  0.005  
12.  _DM(k=3)(H=0)  0.006  
13.  _DM(e=1,d=1)(H=0)  0.004  
14.  _DM(e=1,d=2)(H=0)  0.005  
15.  _DM(e=1,d=3)(H=0)  0.004  
16. 
_DM(H=10)  8  0.016  0.8571396  0 
17.  _DM(k=1)(H=10)  0.01  
18.  _DM(k=3)(H=10)  0.009  
19. 
_DM(e=1,d=1)(H=10)  0.008  
20.  _DM(e=1,d=2)(H=10)  0.012  
21.  _DM(e=1,d=3)(H=10)  0.013  

4.2.1 Experiments and Findings
We can use the expected value of deviation and the worst case burstdeviation latency, defined above, for comparing the shields obtained using various shieldtypes defined in Section 3.4. We synthesized various shields for the correctness requirement given in Example 1 with and the inputoutput propositions . The output propositions of synthesized shield are . For each shield type given in Table 1, the deterministic shields and were synthesized as outlined in the last paragraph of Section 3.3. Here denotes shield synthesized without deviation minimization where as denotes the shield obtained with deviation minimization optimization. The shieldsupervisors were determinized with the preference ordering () on outputs.
Table 3 gives the results obtained. We report the number of states of the shield along with the time taken (in seconds) by the tool DCSynth to compute the shield. Moreover, for comparing the performance of the resulting shields, their Expected Value of nondeviation as well as the worst case burstdeviation latency are reported in the table under the columns titled Expected Value and Latency, respectively.
It is observed that with deviation minimization optimization, several different shield types resulted in identical shields, although the time to synthesize them differed. For example, shields in rows numbered 10 to 15 are identical. We indicate such a situation by merging the corresponding rows to a single cell. We give our findings below.

The shield () is unrealizable as expected. See its description in Section 3.4 for an explanation. All the other shield types are found to be realizable.

For shield synthesis without deviation minimization, we obtain distinct shields with distinct performance for each shield type. The Burst shield () has the poorest performance (expected nondeviation and latency ) as it enforces trivial hard deviation requirement . The best performance is obtained for the newly defined shield type by choosing . This gives as the expected value of nondeviation and worst case latency of cycles. With increased difference the performance degrades. Similarly in stabilizing shield () the performance degrades with increase in the value of
Comments
There are no comments yet.