INPUT_2
...
INPUT
...
...
(a) Upper level
INPUT_2
...
Intrusion_
detection
...
Lock_mode Open_button
... ...
(b) Next level
Figure 5.8: General event forking refinement pattern: the event transition diagram The concrete machine
IN P U T 2 ˆ=refinesIN P U T 2 when in=T RU E end Lock mode =refinesˆ IN P U T 2 when in=T RU E
then lock mode:∈BOOL end Open button =refinesˆ IN P U T when in=T RU E
then in:=F ALSE ∧ open button :∈BOOL end Intrusion detection =refinesˆ IN P U T refines IN P U T when in=T RU E
then in:=F ALSE ∧ intrusion :∈BOOLend
5.3.6 Notes
In some case, there might be usage of parameters when performing the event-forking.
Most of the time, the possible values of parameters are declared through the guards of events. This might cause the guards to be different in the parallelized events. However, the parameters cannot change the state of variables before executing the parameter-involved events. Thus, the parallelized events can still be executed in arbitrary manners. In conclusion, this pattern allows the guards of parallelized events to be different in the case that the differences come only from the parameters.
5.4.2 Illustration
Event When guard Then action
Event_C1 When guard and case1 Then action1
Event_C2 When guard and case2 Then action2 Event
When guard Then action
Event_CN When guard and caseN Then actionN ...
If guard then (case1 xor case2 xor … xor caseN)
Figure 5.9: General case-decomposition refinement pattern: refinement tree diagram Figure 5.9 shows the general refinement tree of the case-decomposition refinement pat-tern. In this tree, an abstract event is copied once and refined by N concrete events.
All the concrete events have distinct guards, since each event’s guard is in the form of conjunction of the guard from the abstract event and its distinct case. Their actions are also distinct for each case. There is an invariant linking to all the concrete events. This invariant is to ensure that the entire state space of cases are covered and the cases are disjoint. The disjointness is crucial if only deterministic actions are allowed for all cases.
The copy of the abstract event is useful when too many cases are introduced in one level.
The cases can be gradually introduced in two or more steps of refinements by gradually introducing cases to the copy.
5.4.3 Transformation to Event-B model
The transformation from this pattern into Event-B model is straightforward. The concrete events must explicitly refine the abstract event. The guard from the abstract event should be preserved, while each abstract event must be introduced with new guard representing each case. The actions of each event should also be modified to reflect the responses for each case.
Event-B specification does not have XOR operator. SinceAxorB = (A∨B)∧ 6(A∧B), the latter form can be used for writing the invariant.
Names of the parallelized events are up to developers.
5.4.4 Constraint
The guard of each concrete should not be contradict with the guard of the abstract event, even though the proof obligation GRD can be discharged due to the inconsistency. The concrete actions must simulate the abstract actions due to the proof obligation SIM.
Because of the proof obligationEQL, ones should carefully apply this pattern, especially when the decomposition is done in more than one step of refinement. The state of variables appearing in the abstract machine must only be changed by the concrete events refining
the abstract event which changes the state of the variables. The cases should be well-decomposed to get adequate responses (actions) for modifying the new variables of each refinement step.
5.4.5 Example
DECISION When decision=TRUE Then decision:=FALSE
Pump_on When decision=TRUE and water_level>H and manual=FALSE Then decision:=FALSE and pump_on:=TRUE
Pump_off When decision=TRUE and water_level<H and manual=FALSE Then decision:=FALSE and pump_on:=FALSE
Do_nothing When decision=TRUE and manual=TRUE Then decision:=FALSE
If decision=TRUE then ((water_level>H and manual=FALSE) xor (water_level<H and manual=FALSE) xor manual=TRUE)
Figure 5.10: An example case-decomposition refinement pattern
Figure 5.10 illustrates the application of the case-decomposition refinement pattern in a water tank system. This system has two inputs: water level and manual mode. If the system is in manual mode, the system will do nothing to let all the decisions are made by its users. If the system is not in the manual mode, when the water level is higher thanH (a constant), the system must turn on the pump to decrease the water. Otherwise, the pump must be turned off.
The upper level of the refinement tree only shows abstract behavior that the system is in the decision phase. In the lower level, all cases are modelled by applying case-decomposition pattern. The eventP umponandP umpof f turn on and turn off the pump respectively according to the water level when the system is not in the manual mode. The event Donothing just transit to next phase to reflect that the system do nothing when it is in the manual mode. An invariant is written to ensure that all the cases are considered.
The lower level of the refinement tree can be transform into the following Event-B model:
Events
P ump on =refinesˆ DECISION
when decision=T RU E ∧ water level > H ∧ manual=T RU E then decision:=F ALSE ∧pump on :=T RU E end
P ump of f =refinesˆ DECISION
when decision=T RU E ∧ water level ≤H∧ manual=T RU E then decision:=F ALSE ∧pump on :=F ALSE end
Do nothing =refinesˆ DECISION
when decision=T RU E ∧ manual=F ALSE then decision:=F ALSE end
Invariant
decision=T RU E ⇒(((water level > H ∧manual=F ALSE)∨
(water level≤H∧manual=F ALSE)∨manual=T RU E)∧
¬((water level > H ∧manual=F ALSE)∧
(water level≤H∧manual=F ALSE)∧manual=T RU E))
5.4.6 Notes
When using more than one refinements to cover all the cases, if it is necessary to refine some concrete events’ guard, the invariant as shown in the pattern might not be sufficient for checking the coverage and the disjointness of cases. In this case, the invariant should cover not only where the pattern is applied, but also every modified concrete event.