1 Introduction
2 Background
2.1 Transition systems
2.2 LTL
-
\(\sigma \models p\) iff p evaluates to true given the assignment \(\sigma [0]\)
-
\(\sigma \models \phi \vee \psi \) iff \(\sigma \models \phi \) or \(\sigma \models \psi \)
-
\(\sigma \models \phi \wedge \psi \) iff \(\sigma \models \phi \) and \(\sigma \models \psi \)
-
\(\sigma \models \lnot \phi \) iff \(\sigma \not \models \phi \)
-
\(\sigma \models X \phi \) iff \(\sigma ^1\models \phi \)
-
\(\sigma \models \phi U \psi \) iff there exists \(i\ge 0\) s.t. \(\sigma ^i \models \psi \) and for all j, \(0\le j < i\), \(\sigma ^j \models \phi \)
-
\(\sigma \models \phi R \psi \) iff for all \(i\ge 0\) \(\sigma ^i \models \psi \) or there exists j, \(0\le j < i\), s.t. \(\sigma ^j \models \phi \)
2.3 Parameter synthesis
2.4 Contract refinement
3 Motivation
3.1 Contract-based design
speed
, representing the physical speed of the system and returns a brake signal, brake
. The system is decomposed into a RedundantSensor that reads the physical value and a ControlUnit that reads the speed from the sensor and produces corresponding control signals to the brakes. As the name suggests, the RedundantSensor is implemented with two redundant Sensors, so that the system works even if one of the sensor fails. In order to analyze the behavior of the system in the presence of failures, we introduce two inputs, fail1
and fail2
, which represent the failures of the two sensors.ControlSystem
as a whole black box with ports to interact with its environment. Then, it is decomposed into RedundantSensor
and ControlUnit
components. The RedundantSensor
is in turn decomposed into two redundant Sensor
subcomponents, two Monitor
subcomponents, and a Selector
. The decomposition also defines how the ports of the component being decomposed are mapped down into the decomposition. For example, the “left” ports of the ControlSystem
are mapped onto the “left” ports of the RedundantSensor
. At the lower level, speed
and fail1
are mapped to the input of first sensor, while the inputs of the second sensor are given by speed
and fail2
.ControlSystem
has a contract speed_control
consisting of the guarantee \(G(\texttt {speed}\ge ~th \rightarrow \texttt {brake})\), where th is a threshold parameter of the system, and the assumption \(\lnot \texttt {fail1}\wedge \lnot \texttt {fail2}\wedge G(\lnot \texttt {fail1}\vee \lnot \texttt {fail2})\), i.e., initially none of the sensors is failing while in every future state it sufficient that one of the two is not failing.ControlSystem
are refined by some contracts of the RedundantSensor
and the ControlUnit
subcomponents. The framework guarantees that, under specific conditions (corresponding to correct contract refinement), if the contracts of the subcomponents hold, then the contract of the parent component also holds.3.2 Need of tightening
ControlSystem
example above. The Selector
component has a contract with assumption “true” and guarantee:current_use
is 1 or 2 depending on whether the output is linked to the output of sensor1 or sensor2 respectively, and switch_current_use
triggers the change of current_use
when the monitor of the current sensor detects a failure. Notice, however, that initially the current sensor is sensor1 and therefore there no need to assume (in the top-level assumption) that \(\lnot \)
fail2
(i.e., that initially sensor2 does not fail).switch_current_use
only triggers the change of current_use
to sensor2 when the monitor of sensor1 detects a failure, given the stronger assumption, it will never switch back to sensor1. Thus, the part \(G((\texttt {current\_use}=2 \wedge \texttt {switch\_current\_use}) \rightarrow X(\texttt {current\_use}=1))\) of the above guarantee is not necessary.4 Tightening of a single contract refinement
4.1 Formal definition
-
\(\underline{Sub}' \preceq C'\)
-
\(C'\preceq C\) and, for every \(C_S\in \underline{Sub}\), \(C_S \preceq C'_S\).
-
\(\underline{Sub}' \preceq C'\)
-
\(\mathcal {A}(C)\models \mathcal {A}(C')\) and, for every \(C_S\in \underline{Sub}\), \(\mathcal {G}(C_S)\models \mathcal {G}(C'_S)\).
4.2 The algorithm
4.3 Generation of the parametric problem
4.3.1 Injecting parameters in the formulas
Formula \(\phi \)
|
\(\textit{Weaken}(\phi )=\langle {\phi ^W,P}\rangle \)
| Evaluation \(\gamma \)
|
\(\gamma (\phi ^W)\)
|
---|---|---|---|
\(a < b\)
|
\(p_1 \rightarrow (a < b) \wedge p_2 \rightarrow (a \le b)\)
|
\(\{p_1, p_2\}\)
|
\(a < b\)
|
\(\{p_1\}\)
|
\(a < b\)
| ||
\(\{p_2\}\)
|
\(a \le b\)
| ||
\(\emptyset \)
|
\(\top \)
| ||
\(\phi _1\wedge \phi _2\)
|
\(p_1 \rightarrow \phi _1^{W} \wedge p_2 \rightarrow \phi _2^{W}\)
|
\(\{p_1, p_2\}\)
|
\(\gamma (\phi ^W_1)\wedge \gamma (\phi ^W_2)\)
|
\(\{p_1\}\)
|
\(\gamma (\phi ^W_1)\)
| ||
\(\{p_2\}\)
|
\(\gamma (\phi ^W_2)\)
| ||
\(\emptyset \)
|
\(\top \)
| ||
\(\phi _1 \vee \phi _2\)
|
\(\phi _1^W \vee \phi _2^W\)
| NA |
\(\gamma (\phi ^W_1) \vee \gamma (\phi ^W_2)\)
|
\(\phi _1~\mathcal {R}~\phi _2\)
|
\(p_1 \rightarrow (\phi _1^{W} \wedge \phi _2^W) \wedge p_2 \rightarrow (\phi _1^W~\mathcal {R}~\phi _2^{W})\)
|
\(\{p_1, p_2\}\)
|
\(\gamma (\phi ^W_1) \wedge \gamma (\phi ^W_2)\)
|
\(\{p_2\}\)
|
\(\gamma (\phi ^W_1)~\mathcal {R}~\gamma (\phi ^W_2)\)
| ||
\(\{p_1\}\)
|
\(\gamma (\phi ^W_1) \wedge \gamma (\phi ^W_2)\)
| ||
\(\emptyset \)
|
\(\top \)
| ||
\(\phi _1~\mathcal {U}~\phi _2\)
|
\(\phi _1^W~\mathcal {U}~\phi _2^W\)
| NA |
\(\gamma (\phi ^W_1)~\mathcal {U}~\gamma (\phi ^W_2)\)
|
\(\lnot \phi _1\)
|
\(\lnot \phi ^S_1\)
| NA |
\(\lnot \gamma (\phi ^S_1)\)
|
Formula \(\phi \)
|
\(\textit{Strengthen}(\phi )=\langle {\phi ^S,P}\rangle \)
| Evaluation \(\gamma \)
|
\(\gamma (\phi ^S)\)
|
---|---|---|---|
\(a \le b\)
|
\(\lnot p_1 \rightarrow (a< b) \wedge \lnot p_2 \rightarrow (a=b) \wedge (p_1\wedge p_2) \rightarrow (a \le b)\)
|
\(\{p_1, p_2\}\)
|
\(a \le b\)
|
\(\{p_2\}\)
|
\(a < b\)
| ||
\(\{p_1\}\)
|
\(a = b\)
| ||
\(\emptyset \)
|
\(\bot \)
| ||
\(\phi _1 \vee \phi _2\)
|
\(\lnot p_1 \rightarrow \phi _1^S \wedge \lnot p_2 \rightarrow \phi _2^S \wedge (p_1\wedge p_2)\rightarrow (\phi ^S_1\vee \phi ^S_2)\)
|
\(\{p_1, p_2\}\)
|
\(\gamma (\phi ^S_1) \vee \gamma (\phi ^S_2)\)
|
\(\{p_2\}\)
|
\(\gamma (\phi ^S_1)\)
| ||
\(\{p_1\}\)
|
\(\gamma (\phi ^S_2)\)
| ||
\(\emptyset \)
|
\(\gamma (\phi ^S_1) \wedge \gamma (\phi ^S_2)\)
| ||
\(\phi _1 \wedge \phi _2\)
|
\(\phi _1^{S} \wedge \phi _2^{S}\)
| NA |
\(\gamma (\phi ^S_1) \wedge \gamma (\phi ^S_2)\)
|
\(\phi _1~\mathcal {U}~\phi _2\)
|
\(\lnot p \rightarrow \phi _2^S \wedge p\rightarrow \phi _1^S~\mathcal {U}~\phi _2^S\)
|
\(\{p\}\)
|
\(\gamma (\phi ^S_1)~\mathcal {U}~\gamma (\phi ^S_2)\)
|
\(\emptyset \)
|
\(\gamma (\phi ^S_2)\)
| ||
\(\phi _1~\mathcal {R}~\phi _2\)
|
\(\phi _1^S~\mathcal {R}~\phi _2^S\)
| NA |
\(\gamma (\phi ^S_1)~\mathcal {R}~\gamma (\phi ^S_2)\)
|
\(\lnot \phi _1\)
|
\(\lnot \phi ^W_1\)
| NA |
\(\lnot \gamma (\phi ^W_1)\)
|
4.3.2 Injecting parameters on the contracts
-
The extended proof obligation for satisfying the top level contract$$\begin{aligned} \bigwedge \limits _{i = 1}^{n} (p_i \rightarrow (\mathsf {A}_i \rightarrow \mathsf {G}_i)) \rightarrow (\mathsf {A}\rightarrow \mathsf {G}) \end{aligned}$$
-
For each \(1 \le j\le n\), we have n extended proof obligations:$$\begin{aligned} \Big (\bigwedge \limits _{i=1 \wedge i \ne j}^{n} (p_i \rightarrow (\mathsf {A}_i \rightarrow \mathsf {G}_i)) \wedge \mathsf {A}\Big ) \rightarrow (p_j \rightarrow \mathsf {A}_j) \end{aligned}$$
4.4 Multiple validity parameter synthesis problem
4.4.1 Compositional approach
4.4.2 Encoding all proof obligations into a single one
4.4.3 Minimal configuration of the parameters
5 Tightening the whole system architecture
5.1 Applying tightening within a system architecture
ControlSystem
, where only the contract speed_control
is defined. This contract is refined by (1) the contract sense
of the redundant sensor, which guarantees that the value passed to the control unit approximates the physical value with a bounded error; (2) the contract sensed_speed_is_present
of the redundant sensor, which guarantees that the value provided by the sensor is always available; (3) the contract speed_control
, which similarly to the system contract guarantees that if the speed is above the threshold, then a brake command is issued. After checking the contract refinement is correct, we are able to apply single top-down tightening on the parent contract speed_control
of the system component in order to simplify the contract refinement. Suppose in this case we do not obtain any simplification and we proceed in a top-down fashion in the decomposition tree.RedundantSensor
where two contracts are defined, sense
and sensed_speed_is_present
(see Fig. 2), which are refined by the contracts of the subcomponents of RedundantSensor
. After the contracts specification and refinement is completed at this level and the check of the correctness of the contract refinements for sense
and sensed_speed_is_present
of component BSCU
is successful, we proceed with tightening these contracts.Selector
component, which as explained in Sect. 3.2 can be simplified. In this situation, independently from the order of tightening the contracts sense
and sensed_speed_is_present
, the result of each one can in principle break the correctness of the other and vice versa. This is due to the fact that the tightening technique proposed in the previous section only ensures the correctness of an individual contract refinement. We call this the problem of sharing contracts.5.2 Parallel tightening of a contract refinement
-
\(\underline{Sub}' \preceq C'\)
-
\(C'\preceq C\) and, for every \(C_S\in \underline{Sub}\), \(C_S \preceq C'_S\).
-
\(Sub_k' \preceq CR_k\), for every k, \(1\le k\le n\)
5.3 Removing the sharing of contracts by duplication
switch
of Selector
and update the refinements as shown in Fig. 3. Finally, we are able to run the single tightening procedure on each refinement in isolation.6 Experimental evaluation
6.1 Details of the implementation
ocra_tighten_contract_refinement
that takes as input an OCRA specification, a contract’s name, a component’s name, and produces as output a number of OCRA specifications containing the tightened versions of the given contract and its subcontracts. The command has an option to allow the user to select the approach to the multiple synthesis problem (see Sect. 4.4), either the compositional approach (Sect. 4.4.1) or the encoding approach (Sect. 4.4.2). Other options in the command deal with the problem of sharing contracts: the user can choose to perform a parallel tightening or duplicate the contracts and run a single top-down tightening. Regarding the parameter synthesis algorithm, we have used as back-end an implementation reported in [7]. Since the synthesis is quite expensive for large number of parameters, we arbitrarily limit the injection to 350 parameters so that only the higher level of the formula structure is considered during weakening/strengthening (i.e., during the recursion of Algorithms 3 and 4, when reaching 350 parameters, the recursion is stopped and subfomulas are considered without modifications). This allows to get a tightening also in cases in which the definitions would produce many more parameters making the synthesis blow up.6.2 Description of benchmarks
6.3 Experimental results
6.3.1 Tightening a single contract refinement
Case study |
\(\#\) Contract refinement | Avg. \(\#\) original subcontracts | Avg. \(\#\) irrelevant contracts |
---|---|---|---|
wbs arch1 | 106 | 9.14 | 4.26 |
wbs arch2 v1 | 68 | 3.47 | 0.82 |
wbs arch2 v2 | 109 | 11.04 | 4.93 |
wbs arch2bis v1 | 68 | 3.47 | 0.77 |
wbs arch2bis v2 | 109 | 11.04 | 5.14 |
wbs arch2bis v3 | 109 | 11.04 | 5.21 |
wbs arch3 | 122 | 11.04 | 4.97 |
wbs arch4 | 122 | 11.04 | 5.17 |
Modified CRs wbs arch2 v1 | 12 | 28 | 22 |
Modified CRs wbs arch3 | 12 | 28 | 22 |
Modified CRs wbs arch4 | 12 | 28 | 22 |
Lift system | 1 | 4 | 0 |
Simple wbs | 1 | 3 | 0 |
wbs arp v1 | 3 | 3.66 | 1.33 |
wbs arp v2 | 4 | 3.25 | 1.25 |
wbs arp v3 | 5 | 3.2 | 1.45 |
wbs arp v4 | 5 | 3.2 | 1.45 |
wbs arp v4.1 | 4 | 3 | 1.45 |
wbs arp v2 ext | 7 | 2 | 1 |
wbs arp v3 ext | 7 | 1 | 0 |
wbs arp v4 ext | 7 | 2 | 1 |
Airbag | 7 | 2.42 | 0 |
Monitors v1 | 1 | 6 | 2 |
Monitors v2 | 1 | 6 | 0 |
gb2 | 1 | 3 | 0 |
Redundant sensors v1 | 3 | 5.66 | 0 |
Redundant sensors v2 | 3 | 5.66 | 0 |
6.3.2 Taking into account shared contracts
6.4 An example of applying tightening on a system architecture
wbs_arch4
which is decomposed into a physical system and a control system. We take one of its contracts never_inadvertent_braking_of_wheel_8
and we apply single tightening. As a result, we obtain 2 tightened variants of this contract refinement. While the new refinements are correct, other contract refinements are broken due to the fact that never_inadvertent_braking_of_wheel_8
shares some subcontracts with other contracts (e.g., never_inadvertent_braking_of_wheel_i
for \(0 \le i \le 7\)) defined in the system component like the subcontract system_validity
from control system component. Then, we run parallel tightening on this contract and we do not get any tightened variant. Therefore, we remove the sharing of contracts by duplication and we obtain two tightened variants as a result. We now take one of these variants and we continue in the decomposition of the contract considering the contract expected_behavior_brake_as_cmd_8
in the ControlSystem
component which is just refined by the subcontract expected_behavior_brake_as_cmd_8
of the BSCU
component. We run just a single tightening on this contract and we do not obtain any simplification.expected_behavior_brake_as_cmd_8
in the BSCU
component which is decomposed into two redundant Channel
, an OrGate
, and a 12 SwitchGate
components. This contract shares several subcontracts with other contracts (e.g., expected_behavior_brake_as_cmd_j
for \(0 \le j \le 7\)) defined in the BSCU
component. The shared subcontracts correspond to different subcomponents, e.g., system_validity
, command_creation_alternate_k
(\(1 \le k \le 4\)), and command_creation_normal_l
(\(1 \le l \le 8\)) of the Channel
component. Also, subcontract or_behavior
of the OrGate
component. We first try with parallel tightening but we do not get any simplification. Then, we remove the sharing of contracts by duplication and we obtain as result that several subcontracts are not needed for the contract refinement. In this case that the subcontracts command_creation_alternate_k
(\(1 \le k \le 4\)) and command_creation_normal_l
(\(1 \le l \le 8\)) are irrelevant. We have investigated the reason and we observe that the contract system_validity
is too weak. Therefore, we manually strengthen the contract and we rerun the procedure of duplication and we observe that now two more contracts channel_1.command_creation_normal_8
and channel_2.command_creation_normal_8
for the two redundant Channel
are relevant for this contract refinement.command_creation_normal_8
from the Channel
component which is refined by the subcontract command_creation_normal_8
of CommandSystem
component. This contract from the Channel
component does not share contracts. By applying tightening, we do not obtain any simplification.Channel
component is decomposed into component MonitorSystem
and CommandSystem
, where the first one is a leaf component which means that we have covered one branch of decomposition and the refinements of contracts from the system component. Subsequently, we tighten the contract command_creation_normal_8
of CommandSystem
component. This component is decomposed in four WheelPairCommandSystem
components. The contract command_creation_normal_8
is refined by contract command_creation
of WheelPairCommandSystem
component. This is shared by contract command_creation_normal_4
of CommandSystem
. Thus, we run parallel tightening on the contract and we do not get any tightened variant. Then, we try by removing the sharing by duplication and we get a simplified version of the contract refinement command_creation_normal_8
. Finally, as CommandSystem
is a leaf component we have covered another branch of decomposition and the contracts refinement from the system component.