A.5 Event-B specification
A.5.5 Third refinement
end END
then
act3: speed:=d end
Event INPUT speed down door closing =b extends INPUT speed down door closing
any d where
grd1: input=TRUE
grd4: door status=close
grd5: d≥speed−max speed down∧d≤speed∧d≥0 grd6: speed checked=FALSE
then
act3: speed:=d end
Event INPUT speed up door opening =b extends INPUT speed up door opening
any d where
grd1: input=TRUE
grd5: d≥speed∧d≤speed+max speed up∧d≤15 grd6: door status=open
grd7: speed checked=FALSE then
act3: speed:=d end
Event INPUT speed down door opening =b extends INPUT speed down door opening
any d where
grd1: input=TRUE
grd5: d≥speed−max speed down∧d≤speed∧d≥0 grd6: door status=open
grd7: speed checked=FALSE then
act3: speed:=d end
Event switch off =b extends switch off
when
grd2: input=FALSE grd3: speed>15
grd4: speed checked=FALSE then
act1: switch:=FALSE
act2: speed checked:=TRUE end
Event RESULT close =b extends RESULT close
when
grd1: switch=FALSE
grd2: speed checked=TRUE then
act2: input:=TRUE
act3: door status:=close act4: speed checked:=FALSE end
Event switch on =b extends switch on
when
grd2: input=FALSE grd3: speed≤15
grd4: speed checked=FALSE then
act1: switch:=TRUE
act2: speed checked:=TRUE end
Event RESULT no request =b refines RESULT
when
grd1: switch =TRUE
grd2: speed checked =TRUE grd3: request =FALSE then
act2: input :=TRUE
act3: door status :=door status act4: speed checked :=FALSE end
Event RESULT request open =b refines RESULT
when
grd1: switch =TRUE
grd2: speed checked =TRUE grd3: request =TRUE
grd4: door status =close then
act2: input :=TRUE act3: door status :=open act4: speed checked :=FALSE end
Event RESULT request close =b refines RESULT
when
grd1: switch =TRUE
grd2: speed checked =TRUE grd3: request =TRUE
grd4: door status =open then
act2: input :=TRUE act3: door status :=close act4: speed checked :=FALSE end
Event Request =b extends INPUT
when
grd1: input=TRUE then
act1: input:=FALSE act2: request :∈BOOL end
END
Appendix B
Automatic gate controller case study
B.1 Refinement tree diagram
skip
INPUT When input=TRUE Then input:=FALSE
DECISION When input=FALSE Then input:=TRUE INPUT_2
When input=TRUE Then skip
<<parallel>>
INPUT_2 When input=TRUE Then skip
If input=TRUE then Either has card or not
INPUT_hasCard When input=TRUE Then has card or not
INPUT_uid When input=TRUE and hasCard=TRUE Then get uid from the card and input:=FALSE
INPUT_notHasCard When input=TRUE and hasCard=FALSE Then input:=FALSE
If input=FALSE then Has authorized card xor
not has card xor has unauthorized card
DECISION_can_enter When input=FALSE and hasCard and uid of the card is authorized Then can enter and input:=TRUE
DECISION_cannot_enter When input=TRUE and (not hasCard or uid of the card is not authorized) Then cannot enter and input:=TRUE
DECISION When input=FALSE Then input:=TRUE
A
B
C D E F
G
111
INPUT_swipe When input=TRUE Then card is swiped or not
INPUT_uid When input=TRUE and card is swiped Then put uid of the card to buffer and input:=FALSE
INPUT_not_swipe When input=TRUE and card is not swiped Then input:=FALSE Card is swiped = has card
Card is not swiped = not has card
Put uid of the card to buffer = get uid from the
card INPUT_2
When input=TRUE Then skip
A B
C D
INPUT_sensor When input=TRUE Then sensor checks the status of the gate
INPUT_swipe When input=TRUE Then card is swiped or not
INPUT_uid When input=TRUE and card is swiped Then put uid of the card to buffer and input:=FALSE
INPUT_not_swipe When input=TRUE and card is not swiped Then input:=FALSE INPUT_time
When input=TRUE Then checks time
INPUT_sensor When input=TRUE Then sensor checks the status of the gate
INPUT_swipe When input=TRUE Then card is swiped or not INPUT_time
When input=TRUE Then checks time
INPUT_uid When input=TRUE and card is swiped Then put uid of the card to buffer and input:=FALSE
INPUT_not_swipe When input=TRUE and card is not swiped Then input:=FALSE
112
DECISION When input=FALSE Then input:=TRUE DECISION_open
When input=FALSE and card is swiped and uid in the buffer is in AuthDB Then send “open” command to gate
and input:=TRUE
DECISION_lock When input=FALSE and (card is not swiped or uid in the buffer is not in AuthDB) Then send “lock” command to gate and input:=TRUE
If sending “open”
command to gate then Can enter
If sending “lock”
command to gate then Cannot enter E
F G
DECISION_open When input=FALSE and card is swiped and uid in the buffer is in AuthDB Then send “open” command to gate and input:=TRUE and restart timer
DECISION_lock When input=FALSE and (card is not swiped or uid in the buffer is not in AuthDB) and the ‘open’ command has been sent for more than 5 seconds
Then send “lock” command to gate and input:=TRUE
DECISION_do_nothing When input=FALSE and (card is not swiped or uid in the buffer is not in AuthDB) and the ‘open’ command has been sent for less than 5 seconds Then input:=TRUE
DECISION_reset_time When input=FALSE and (card is not swiped or uid in the buffer is not in AuthDB) and gate is locked Then input:=TRUEand restart timer If input=FALSE then
All combination of inputs are considered
DECISION_open When input=FALSE and card is swiped and uid in the buffer is in AuthDB Then send “open” command to gate and input:=TRUE and restart timer and alarm is off
DECISION_lock When input=FALSE and (card is not swiped or uid in the buffer is not in AuthDB) and the ‘open’ command has been sent for more than 5 seconds but less than 15 seconds
Then send “lock” command to gate and input:=TRUE
DECISION_do_nothing When input=FALSE and (card is not swiped or uid in the buffer is not in AuthDB) and the ‘open’ command has been sent for less than 5 seconds Then input:=TRUE and alarm is off
DECISION_reset_time When input=FALSE and (card is not swiped or uid in the buffer is not in AuthDB) and gate is locked Then input:=TRUEand restart timer and alarm is off DECISION_alarm_on
When input=FALSE and (card is not swiped or uid in the buffer is not in AuthDB) and the ‘open’ command has been sent for more than 15 seconds
Then send “lock” command to gate and input:=TRUE and alarm is on If input=FALSE and (card is not
swiped or uid in the buffer is not in AuthDB) and gate is opened then
gate is opened more than 5 seconds but less than 15 seconds
or more than 15 seconds
113