"Modeling in Event-B: System and Software Engineering" Cambridge University Press Abrial : http://www.cambridge.org/ (http://www. gb/knowledge/isbn/item2710130/?site_locale=en_GB event-b.org/A_errata.pdf) The original book "Modeling in Event-B: System and Software Engineering" is in copyright, that the translation appears with permission of the Author of Cambridge University Press.  This translation should not be sold or resold. See also following webpage for more information about the original book: http://www.cambridge. org/gb/knowledge/isbn/item2710130/?site_locale=en_GB. This translation corresponds with the errata sheet for the original book: http://www.event-b.org/A_errata.pdf . Modeling in Event-B: System and Software Engineering B : Jean-Raymond Abrial 2011 9 14 2 1 2 3 4
5
6 7 2 1 : (external observer) (correct) (correct by construction) ( ) (proof obligation rule) *1 (rules of inference of the sequent (propositional logic) (equality) calculas) (basic arithmetic) ( 4 (4 7 ) 2 ) 33 3 2 (environment) (controller) 2 ENV FUN .1 :
statement sentence 1 5 (closed model) (as well as its environment) (correct) 7 [FUN-1] 2 2 2 [ENV-1] [ENV-2] [ENV-3] 2 4 [ENV-4] 4 2 2 [ENV-5] 1*2 [FUN-2] [FUN-3]じ: 3 . FUN-2 (4  ) FUN-2 . . . [FUN-3] ENV-1, ENV-2, ENV-3 (7 ) [ENV-4, ENV-5] (5  ) (6 ) (architecture) FUN-1 FUN-1 4 4.1 (compound) (far more abstruct) ML out ML in 2 (state) (4.2 ) (events) (4.3 ) 4.2 (static part) (dynamic part) (constant) (variable) (context) axm0_1 axm0_1 : d ∈ N : d n inv0_1 : n ∈ N inv0_2: n ≤ d (invariant) inv0_1 inv0_2 2 inv0_1 n inv0_2 n (first basic requirement) FUN-2 inv0_2 axm0_1, inv0_1, inv0_2 (invariant) axm (axiom) inv 0 inv0_2 2 2 2 d d : n n n axm inv 4.3 2 (events) ML_out 3 ML_out 4 ML in 1 (first approximation) ML_out n := n + 1 ML  in n := n − 1 n := n − 1 ML_in, ML_out (action) (actions) (we are not programming)
1 1. (incremental fashion) (we are not programming) 2. 4.4 (before-after predicate)
= !! n (by convention)   n' (just before) n (just after) ML_out n 1 n' = n + 1 (deterministic) 4.5 ML out ML in inv0_1 inv0_2 n (it has to be proved in a rigorous fashion) INV (proof obligation) INV (verification condition) c A(c) c A 1 (c), A 2 (c), ... A(c) axm0_1 v I(c,v) 2 I(c, v) A(c) I(c,v) I 1 (c, v), I 2 (c, v), ... inv0_2 I(c,v) I i (c, v) ν′ = E(c,v) inv0_1 A(c), I(c, v) F I i(c, E(c, v)) [INV] *3 (sequent) I(c,v) I i (c, E (c, v)) A(c) I i (c, v) (entail) A(c) I(c,v) v E(c,v) (invariant) INV A(c) I(c, v) F I i (c, E (c, v)) [INV] C c A(c) I(c,v) I i (c, E (c, v)) I i (c,v) INV F [INV] INV (what we have to formally prove) 4.11 4.8 INV (Proof Obligation Generator) 4.6 =4 (sequent) H - G
(hypotheses) G
G H (under) 4.7 INV 4 2 2 (ML_out, ML_in) (inv0_1, inv0_2) (compound names) INV ×5 4な9 !
5 2 ML_out / inv0_1 / INV ML_out / inv0_2 / INV ML_in / inv0_1 / INV ML in / inv0 2 / INV INV 2 2 ML out inv0_1
T ML in n' = n − 1 T ML in T 4.8
t n + 1 ∈ N ML_out / inv0_1 / INV
ML_in ML_in / inv0_1 / INV
n − 1 ∈ N
F
F
n + 1 ≤ d F (transformation) d ∈ N n ∈ N n ≤ d T n + 1 ∈ N ...(1) (irrelevant hypotheses) ( d ∈ N n ≤ d n + 1 ∈ N ) n ∈ N + n + 1 ∈ N ...(2) (sufficient) (2) (2) (2) (1) (1) n n + 1 4.9 (rules of inference) H1 F G —MON— H1, H2 F G ) 1 (antecedents) ( : (monotonicity) ) MON ( 1 (consequent) G 2 H1 H2 G H1 H2 H2 H1 (1) H2 d ∈ N n ≤ d d ∈ N, n ∈ N, n ≤ d 2 n ∈ N —P2— H, n ∈ N + n + 1 ∈ N 2
H *6 (axiom)
—P2— n ∈ N + n + 1 ∈ N —P2’— 0 < n ৮ n − 1 ∈ N ( : 0 n n – 1
INC 2 n —INC— n < m ৮ n + 1 ≤ m INC n m n + 1 m —DEC— n ≤ m ৮ n − 1 < m DEC n m
m P2’,INC, DEC (derived) (library) 4.10 H1, H2, G, n, m (meta-variables) (match) P2 *  : axiom —P2— n ∈ N + n + 1 ∈ N 2 a + b ∈ N + a + b + 1 ∈ N n a + b (matching) 4.11 4.24
4.8 *8 d ∈ N n ∈ N n ≤ d F
t n + 1 ∈ N —P2—
INC n ≤ d
F
t
0 < n .8 : n ∈ N P2’ d ∈ N n ∈ N n ≤ d F n − 1 ∈ N —MON— n ∈ N F n − 1 ∈ N —?— ML_in / inv0_2 / INV d ∈ N n ∈ N n ≤ d - n − 1 ≤ d —MON— n ≤ d F n − 1 < d V n − 1 = d —OR R1— n ≤ d F n – 1 < d —DEC— 2 n − 1 ≤ d     n − 1     d n − 1 < d V n − 1 = 0 OR_R1 ( ） n – 1 < d (or) d v DEC 4.12 OR_R1 OR_R1 OR R2 H F P —OR R1— H F P V Q H F Q —OR R2— H F P V Q 9* 199 9 2
(obvious) R1 R2 R T (right) (left) L 4.13 : a bug) (a failed proof reveals (necessary condition) (guards) ML_out ML in n < d 0 < n n d n
then n := n − 1 end when then 1 then end 4.14 G(c,v) ν′ = E(c,v) G(c,v) ( c
4.5 INV ) A(c) I(c, v) G(c,v) F I i (c, E (c, v)) [INV] F [INV] 4.15 INV ML_out inv0_2
ML out inv0_2
n + 1 ≤ d ML_out / inv0_2 / INV inv0_1
T ML_in / inv0_1 / INV
4.11 ML_out / inv0_1 / INV ML in / inv0 2 / INV MON (4.9  ) (less) 4.16 ML_in, ML_out inv0_1, inv0_2 init init n := 0 init (initializing) := init n n' = 0 n' 4.17 init init (establish the invariant) 4.5 INV c A(c) v I(c, v) INV ν′ = K(c) A(c) T I i (c, K(c)) [INV] F [INV] 4.18 axm0_1 F
inv0_1 / INV F axm0_1 F
F
inv0_2 / INV 4.19 1 0 : P1 —P1— F 0 ∈ N 2 0 —P3— n ∈ N F 0 ≤ n 2 4.20 ML in ML out (deadlock) 3 0 P3 2 [FUN-4] 4.21 v c A(c) G 1 (c, v), G 2 (c, v), ..., G m (c, v) I(c,v) DLF c A(c) I(c, v) A(c) I(c, v) F G 1 (c, v) V ... V G m (c, v) [DLF] F [DLF] (not mandatory) 4.22 DLF
4.23 (proof ob cases) OR R 2 v P P V Q (prove independently) Q H, P F R   H, Q F R —ORL— H, P V Q F R 4.12
H F Q —OR_R2— H F P V Q
FALSELL
—FALSE L— T F P 2 H(F), E = F Þ P(F) —EQ LR— H(E), E = F Þ P(E)
e H(E) H(E), E = F Þ P(E) —EQ-RL— H(F), E = F Þ P(F)
H(F) F
E
H(E) P(E) E e —EQL— F E = F 4.24 DLF *10 d ∈ N n ∈ N n ≤ d F n < d V 0 < n DLF n ≤ d n < d V n = d OR_L 2 *11 OR L d ∈ N n ∈ N n < d V n = d F n < d V 0 < n —MON— n < d V n = d F n < d V 0 < n —ORL— ... … —ORL— n < d F
◆10 axm0_2 axm0_2: 0 < d FUN-2 [FUN-2] d 0 MON (4.9  ) 4.25 ( ) d ) ( ) (4.13 : d axm0_1: d ∈ N axm0_2: d > 0 : n inv0_1 : n ∈ N inv0_2: n ≤ d
5 1 5.1 (refinement) (prove) IL out ML out IL in ML  in 5 5.2 n (replaced by three variables) 3 n 3 a, b, c c 6 (abstruct state) (concrete state) a, b, c n (abstract variable) (concrete variables) (concrete invariants) a, b, c inv1_1, inv1_2, inv1_3 inv1_1: a ∈ N inv1_2: b ∈ N inv1_3: c ∈ N inv1_4: a + b + c = n inv1_5: a = 0 V c = 0 : a, b, c inv1_4 a, b, c a, b, c FUN-3 inv1_5 (inv1_1, inv1_2, inv1_3, inv1_5) inv1.4 1 d d a b n n 0 a c 0 c a a c 0 5.3
a, b, c ML in, ML out c = 0 ML out a + b < d 2 33 a, b, c
1 c 1 0 < c 1 c a 0 1 c 0 c ML out a 1 0 a + b < d d a + b + c < d 5.4 (several variables)
a' = a + 1b' = bc' = c c := c + 1 a' := a+1 c' = c + 1 b' = b α′ = a 5.5 (to refine its abstraction) 2 ML out
(not contradictory) a + b < d           c = 0     a + b + c < d n < d
inv1_4
ML in n 
ML out 5.6 (stronger) (impliy) 5.16 w c
v I(c, v) G(c,v) H(c,w) J(c,v,w) G(c,v) G 1 (c, v), G 2 (c, v) . . . G i (c,v) A(c) I(c, v) J(c,v,w) H(c,w) F G i (c,v) [GRD] T [GRD] v w J(c,v,w) w J(c,v,w) J(c,v,w) w w v' ν*12 v w J(c,v',w') v J(c,v,w) w ( ) INV J(c, v, w) 1 J i (c, v, w) A(c) I(c, v) J(c,v,w) H(c,w) t J i (c, E (c, v), F (c, w)) [INV] T [INV] 5.7 ML in ML out GRD +12 : ML out ML_out
MON c = 0 a + b < d a + b + c = n n < d
a + b + c = n a + b < d c = 0 F n < d —EQ-LR— a + b + 0 = n [ARI] a + b < d F n < d —ARI— a + b = n a + b < d F n < d —EQ_LR— n < d F n < d —HYP— ARI *13 ML_in MON b ∈ N a + b + c = n a = 0 V c = 0 0 < c F 0 < n b ∈ N a + b + c = n a = 0 V c = 0 0 < c F 0 < n —OR L— ... +13
—ARI— 0 < n F 0 < n —HYP— INV 2 5 10 ML out inv1_4 MON a + b + c = n T a + 1 + b + c = n + 1 [ARI] —ARI— a + b + c = n F a + b + c + 1 = n + 1 —EQ_LR—ﾋn + 1 = n + 1 —EQL—
30
ML in inv1_5 MON a = 0 V c = 0 0 < c F a = 0 V c − 1 = 0 —ORL— ... … —ORL— a = 0 0 < c F a = 0 V c − 1 = 0 —OR R1— a = 0 0 < c F a = 0 —MON— a = 0 T a = 0 —HYP— 5.8 init init init a := 0 b := 0 c := 0 (multiple action) α′ = 0 ∧ b′  = 0 ∧ c′  = 0 5.9 init init INV w' = L(c) : —OR L— c = 0 0 < c F a = 0 V c − 1 = 0 —EQ_LR— 0 < 0 [ARI] F a = 0 V c − 1 = 0 —ARI— l r a = 0 v c − 1 = 0 —FALSE L— ν ′ = K(c) A(c) F J i (c, K (c), L (c)) L 5.10 5
inv1_4

inv1_5
5.11
ML_in
(multiple actions) ML_out a α′ = a − 1 ∧ b′ = b + 1 ∧ c′ = c a' = a ∧ b' = b − 1 ∧ c' = c + 1 IL in a b 0 < a IL out b c IL out 2 0 < b a = 0 5.12 skip (does nothing) skip skip n n' = n skip 3 a, b, c α′ = a ∧ b′ = b ∧ c′ = c 5.13 (5.11 ) ML_in ML_out skip INV IL_in inv1_4
a + b + c = n a = 0 V c = 0 0 < a
inv1_5 ML in F F a − 1 + b + 1 + c = n inv1_4 n skip MON a + b + c = n F a − 1 + b + 1 + c = n [ARI] —ARI— a + b + c = n t a + b + c = n —HYP— IL in inv1  5 ... …
F a − 1 = 0 V c = 0 MON a = 0 V c = 0 0 < a F a − 1 = 0 ∨ c = 0 —OR L— …
IL out 5.14 (do not diverge) (enabled) (indefinitely) ML out ML in (existing) (variant) events) 2 2 1 (decreased by all new
) A(c) I(c, v) J(c,v,w) H(c,w) F V(c, w) ∈ N [NAT] F [NAT] 2 H(c,w) V(c, w) w' = F(c,w) A(c) I(c, v) J(c,v,w) H(c,w) F V(c, F(c, w)) < V(c, w) [VAR] F < [VAR] (same 1 variant) 5.15 variant_1 : 2 * a + b
VAR IL out
2 × a + b − 1 < 2 × a + b 5.16 ( ) G 1 (c, v), . . , G m (c, v) DLF H 1 (c, w), . . , H n (c, w) A(c) I(c,w) J(c,v,w) G 1 (c, v) V . . . V G π (c, v) F H 1 (c, w) V ... V H n (c, w) [DLF] F [DLF] 5.17 DLF
DLF (a + b < dc = 0) V c > 0 V a > 0 V (b > 0a = 0) 5.18 (disjunction) ( ) *14
+14 : 2 (ANDLL) (AND R) H, P, Q F R —AND L— H, P ∧ Q F R H F P  H F Q —AND R— H F P V Q (MON ) 0 < d a ∈ N b ∈ N c ∈ N F (a + b < d ∧ c = 0) ∨ c > 0 ∨ a > 0 ∨ (b > 0 ∧ a = 0) —OR R— 0 < d a ∈ N b ∈ N c ∈ N [ARI] ¬(c > 0) [ARI] L (a + b < d ∧ c = 0) ∨ a > 0 ∨ (b > 0 ∧ a = 0) —ARI— 0 < d a ∈ N b ∈ N c = 0 F (a + b < d ∧ c = 0) ∨ a > 0 ∨ (b > 0 ∧ a = 0) —EQ LR— 0 < d a ∈ N b ∈ N F (a + b < d ∧ 0 = 0) ∨ a > 0 ∨ (b > 0 ∧ a = 0) —OR R—
38
0 < d a ∈ N [ARI] b ∈ N ¬(a > 0) [ARI] F (a + b < d ∧ 0 = 0) ∨ (b > 0 ∧ a = 0) —ARI— 0 < d b ∈ N a = 0 F (a + b < d ∧ 0 = 0) ∨ (b > 0 ∧ a = 0) —EQ_LR— 0 < d b ∈ N [ARI] F (0 + b [ARI] < d ∧ 0 = 0) ∨ (b > 0 ∧ 0 = 0) —ARI— 0 < d b = 0 V b > 0 F (b < d ∧ 0 = 0) ∨ (b > 0 ∧ 0 = 0) —OR L— … ... —OR L— 0 < d b = 0 F (b < d ∧ 0 = 0) ∨ (b > 0 ∧ 0 = 0) —OR R1— 0 < d b = 0 F b < d ∧ 0 = 0 —EQ_LR— 0 < d F 0 < d ∧ 0 = 0 —AND  R— … ... —AND_R— 0 < d F 0 < d —HYP— ...
—OR L—
F (b < d ∧ 0 = 0) ∨ (b > 0 ∧ 0 = 0) —OR_R2— 0 < d,b > 0 F b > 0 ∧ 0 = 0 —AND R— ...

39
5.19 1 1 : d : a,b,c
inv1_5: a = 0 V c = 0 1
end init a := 0 b := 0 c := 0 6 2 ( ML out) ( IL out) 2 7 ml_tl il_tl 6.1 (green) : COLOR : red, green 2 COLOR ( red ) axm2_1 : COLOR = {green, red} axm2_2 : green ≠ red ) ml_tl ll l out inv2_1 : ml_tl ∈ COLOR inv2_2: il_tl ∈ COLOR inv2_3: ml_tl = green ⇒ a + b < d ∧ c = 0 inv2_4: il_tl = green ⇒ 0 < ba = 0 : ...
inv2_3 inv2_4 (conditional invariants) → 6.6 a, b, c n ml_tl il_tl (superposition) a, b, c 6.4 6.2 ML out IL out ENV-3 IL in ML out 2 ) ml_tl ( il_tl ( inv2_1 inv2_2 2 (conditional invariants) inv2_3 inv2_4 ML out il_tl ENV_1, ENV_2, ENV_3 ML in
IL out (  when a := 0 0 < b then b,c := b − 1,c + 1 end 6.3 2 ML out IL out
6.4 : INV u  I(c,u,v) v     w J(c, u, v, w) (completely disjoint)
(  when il_tl = green then b,c := b − 1,c + 1 v INV v V 1 v1 = v (adding the additional concrete invariant) u' = E(c,u,v) ν = M(c,u,v) w' = F(c,v,w) H(c,v,w) ν′ = N(c,v,w) INV 2
F F J i (c, E (c, u, v), M (c, u, v), F (c, v 1 , w)) M (c, u, v) = N (c, v 1 , w) v1 = v v V1 V1 INV INV *15 J(c, u, v, w)
J(c,u,v,w) H(c,v,w) F J(c, E(c, u, v), M(c, u, v), F(c, v, w)) M(c,u,v) = N(c,v,w) INV SIM A(c) I(c, u, v) J(c, u, v, w) H(c,v,w) F M(c, u, v) = N(c, v, w) [SIM] F [SIM] 6.5 *16 INV +15 ●16 : : GRD, SIM,
J(c, u, v, w) IL in ML in INV SIM GRD inv2_3 inv2_4 SIM ML out IL  out GRD
IL_out ML_out INV 6.6 H, P, Q F R —IMP_L— H, P, P ⇒ Q F R H, P F Q —IMP_R— H F P ⇒ Q H, ¬Q ÷ P —NOT_L— H, ¬P ÷ Q 6.7 ML out inv2_4 2 *17 9 +17
(MON ) green ≠ red il_tl = green ⇒ 0 < b ∧ a = 0 ml tl = green F il_tl = green ⇒ 0 < b ∧ a + 1 = 0 —IMP_R— green ≠ red il_tl = green ⇒ 0 < b ∧ a = 0 ml_tl = green il_tl = green F 0 < b ∧ a + 1 = 0 —IMP_L— green ≠ red 0 < b ∧ a = 0 ml tl = green il_tl = green F 0 < b ∧ a + 1 = 0 —ANDL— green ≠ red 0 < b a = 0 ml tl = green il_tl = green F 0 < b ∧ red —AND   R— …
(MON ) green ≠ red ml_tl = green ⇒ a + b < d ∧ c = 0 il_tl = green F ml tl = green ⇒ a + b − 1 < d ∧ c + 1 = 0 —IMP_R— green ≠ red ml_tl = green ⇒ a + b < d ∧ c = 0 il_tl = green ml tl = green F a + b − 1 < d ∧ c + 1 = 0 —IMP_L— green ≠ red a + b < d ∧ c = 0 il_tl = green ml tl = green F a + b − 1 < d ∧ c + 1 = 0 —AND_L— green ≠ red a + b < d c = 0 il_tl = green ml tl = green F a + b − 1 < d ∧ c + 1 = 0 —AND_R— …
47

—ARI— green ≠ red il_tl = green ml_tl = green F
2 green ≠ red il_tl = green ml_tl = green F 1 = 0 (obvious fact) inv2_5: ml_tl = red V il_tl = red ENV-3 (not both at the same time) FUN-3 green ≠ red ml_tl = red V il_tl = red il_tl = green ml tl = green F l = 0 —OR L— …
ML_tl_green IL_tl_green inv2_5 6.3 *18 ML_tl_green IL tl_green
+18 :
49
…
ml_tl = green ⇒ a + b < d ∧ c = 0 il_tl = green ⇒ 0 < b ∧ a = 0 ml_tl = green F ml_tl = green ⇒ a + 1 + b < d Λ c = 0
F inv2_3 (MON ) ml_tl = green ⇒ a + b < d ∧ c = 0 F ml_tl = green ⇒ a + 1 + b < d ∧ c = 0 —IMP_R— ml_tl = green ⇒ a + b < d ∧ c = 0 ml_tl = green F a + 1 + b < d ∧ c = 0 —IMP_L— a + b < d ∧ c = 0 ml tl = green F a + 1 + b < d ∧ c = 0 —AND L— a + b < d c = 0 ml_tl = green F a + 1 + b ∧ c = 0 —AND_R— … … —AND„R— a + b < d F
c = 0 F c = 0 —HYP— 2 a + 1 + b      d ml_tl 1 d FUN-3 ML out 2 ) ML_out_1
IL out b inv2_4
IL out inv2_4 *19 ML out IL out IL out_1
(
6.8 a c 0 ML_tl_green IL_tl_green (     ) + 19 :
*20
TRUE : ... ml_pass, il_pass inv2_6 : ml_pass ∈ BOLL inv2_7 : il_pass ∈ BOOL ML_out_1, ML_out_2, IL_out_1, IL_out_2 ml_pass TRUE il pass
+20 : ML_tl_green IL_tl_green ml_pass il pass FALSE il_pass = TRUE ml_pass = TRUE ML_tl_green when ml_tl = red a + b < d c = 0 il_pass = TRUE [New!] then ml_tl := green il_tl := red ml_pass := FALSE[New!] end IL tl_green when il_tl = red 0 < b a = 0 ml_pass = TRUE [New!] then il_tl := green ml_tl := red il_pass := FALSE end variant_2 : ml_pass + il_pass ml_pass il_pass BOOL b 2 n axm2_3: b_2_n ∈ BOOL → {0, 1} axm2_4: b_2_n(TRUE) = 1 axm2_5*²¹ : b_2_n(FALSE) = 0 :... b 2 n variant_2 : b_2_n(ml_pass) + b_2_n(il_pass) ML_tl_green IL_tl_green VAR ml_tl = red a + b < d c = 0 il_pass = TRUE F b_2_n(il_pass) < b_2_n(ml_pass) + b_2_n(il_pass) il_tl = red b > 0 a = 0 ml_pass = TRUE b_2_n(ml_pass) < b_2_n(ml_pass) + b_2_n(il_pass) axm2.4 {0, 1} F →21 2 2 axm2.5 :
53
1
ml_pass = TRUE
2 il_pass = TRUE inv2_8 : ml_tl = red ⇒ ml_pass = TRUE inv2_9: il_tl = red ⇒ il_pass = TRUE inv2_9 inv2_8 6.9 DLF ( ) d ∈ N 0 < d ml材∈ COLOR il_tl ∈ COLOR ml_pass ∈ BOOL il_pass ∈ BOOL a ∈ N b ∈ N c ∈ N ml_tl = red ⇒ ml_pass = TRUE il_tl = red ⇒ il_pass = TRUE F (ml_il = red ∧ a + b < d ∧ c = 0 ∧ ml_pass = TRUE ∧ il_pass = TRUE) ∨ (il_il = red ∧ a = 0 ∧ b > 0 ∧ ml_pass = TRUE ∧ il_pass = TRUE) ∨ ml_tl = green ∨ il_tl = green ∨ a > 0 ∨ c > 0 [DLF] *22 —— d ∈ N 0 < d b ∈ N ml_tl = red il_tl = red ml_tl = red ⇒ ml_pass = TRUE il_tl = red ⇒ il_pass = TRUE F (b < d ∧ ml_pass = TRUE ∧ il_pass = TRUE) ∨ (b > 0 ∧ ml_pass = TRUE ∧ il_pass = TRUE) -l *22 : —!— d ∈ N 0 < d b ∈ N ml tl = red il_tl = red ml_pass = TRUE il_pass = TRUE F (b < d ∧ ml_pass = TRUE ∧ il_pass = TRUE) ∨ (b > 0 ∧ ml_pass = TRUE ∧ il_pass = TRUE) -l 0 < d b ∈ N F b < d v b > 0 —OR R1— 0 < d b = 0 F b < d —EQ-LR— 0 < d F 0 < d —HYP— 6.10 2 ( 4 2 : ... ml_tl il_tl ml_pass il_pass ) 4 2 inv2_1: ml_tl ∈ COLOR inv2_2: il_tl ∈ COLOR inv2_3: ml_tl = green ⇒ a + b < dc = 0 inv2_4: il_tl = green ⇒ 0 < ba = 0 inv2_5: ml_tl = red V il_tl = red inv2_6 : ml_pass ∈ BOOL inv2_7 : il_pass ∈ BOOL inv2_8 : ml_tl = red ⇒ ml_pass = TRUE inv2_9 : il_tl = red ⇒ il_pass = TRUE variant_2: b_2_n(ml_pass) + b_2_n(il_pass) 2
7 3 7.1 8 ( ) (software controller) (physical 9 ( ) environment) (channels) 2 (closed model) *23 a, b, c il_pass ml_pass a, c b a, b, c “off” “on” “off” “on” : ML_OUT_SR, ML_IN_SR, IL_OUT_SR, IL_IN_SER (phisical variables) 4 A, B, C 3 B (physical) A C ml_tl il_tl +23 4 7.2 ( ) 2 “off” “on” ) “on” 10 ( ) : ml_out_10, ml_in_10, 4 il_in_10, il_out_10 : ml_out_10, ml_in_10, il_in_10, il_out_10 : a,b,c,ml_pass,il_pass : ml_tl , il_tl : A, B, C, ML_OUT_SR, ML_IN_SR, IL_OUT_SR, IL_IN_SR 11 ( ) 7.3 7.2 (“on” “off”) : ..., SENSOR : . . . , on , off axm3_1 :  SENSOR = { on, off} axm3_2: on ≠ off inv3_1: ML_OUT_SR ∈ SENSOR inv3_2: ML_IN_SR ∈ SENSOR inv3_3: IL_OUT_SR ∈ SENSOR inv3_4: IL_IN_SR ∈ SENSOR inv3_5: A ∈ N inv3_6:  B ∈ N inv3_7: Ｃ ∈ N inv3_8: ml_out_10 ∈ BOOL inv3_9 : ml_in_10 ∈ BOOL inv3_10 : il_out_10 ∈ BOOL inv3_11: il_in_10 ∈ BOOL IL IN SR on 1 IL_IN_SR IL OUT SR ML_IN_SR 3_12 : IL_IN_SR = on ⇒ A > 0 3_13 : IL_OUT_SR = on ⇒ B > 0 3_14 : ML_IN_SR = on ⇒ C > 0 TRUE ml_out_10 ML_OUT il_out_10 2 3_15 : ml_out_10 = TRUE ⇒ ml_tl = green 3_16 : il_out_10 = TRUE ⇒ il_tl = green 3_17: IL_IN_SR = on ⇒ il_in_10 = FALSE 3_18 : IL_OUT_SR = on ⇒ il_out_10 = FALSE 3_19: ML_IN_SR = on ⇒ ml_in_10 = FALSE 3_20: ML_OUT_SR = on ⇒ ml_out_10 = FALSE 2 (A) (B) (A) (B) (this assumption has to be checked when installing the system) [FUN-5] (A, B, C) (a, b, c) A 1 3_21: il_in_10 = TRUE ∧ ml_out_10 = TRUE ⇒ A = a 3_22 : il_in_10 = FALSE ∧ ml_out_10 = TRUE ⇒ A = a + 1 3_23 : il_in_10 = TRUE ∧ ml_out_10 = FALSE ⇒ A = a − 1 3.24: il_in_10 = FALSE ∧ ml_out_10 = FALSE ⇒ A = a il_in_10 = TRUE
B a b ml_out_10 = TRUE
A 1 a B b C c 3_25 : il_in_10 = TRUE ∧ il_out_10 = TRUE ⇒ B = b 3_26 : il_in_10 = TRUE ∧ il_out_10 = FALSE ⇒ B = b + 1 3.27 : il_in_10 = FALSE ∧ il_out_10 = TRUE ⇒ B = b − 1 3.28 : il_in_10 = FALSE ∧ il_out_10 = FALSE ⇒ B = b 3_29 : il_out_10 = TRUE ∧ ml_in_10 = TRUE ⇒ C = c 3_30 : il_out_10 = TRUE ∧ ml_in_10 = FALSE ⇒ C = c + 1 3_31 : il_out_10 = FALSE ∧ ml_in_10 = TRUE ⇒ C = c − 1 3_32: il_out_10 = FALSE ∧ ml_in_10 = FALSE ⇒ C = c 2 number of cars) 2 ( ) (hold for the physical 3_33: A = 0 V C = 0 3_34: A + B + C ≤ d A, B, C a, b, c ) ( A, B, C 7.3 ML_out_1 when ml_out_10 = TRUE [New!] a + b + 1 ≠ d then a := a + 1 ml_pass := TRUE ml_out_10 := FALSE [New!] end ML_out_2 when ml_out_10 = TRUE [New!] a + b + 1 = d then a := a + 1 ml_tl := red ml_pass := TRUE ml_out_10 := FALSE [New!] end
IL out 2 when il_out_10 := TRUE [New!] b = 1 then b := b − 1 c := c + 1 il_tl := red il_pass := TRUE il_out_10 := FALSE end il_out_10 ml_out_10 inv3_15 inv3_16 ML in when ml_in_10 = TRUE [New!] c > 0 then c := c − 1 ml_in_10 := FALSE [New!] end IL in when a > 0 il_in_10 = TRUE [New!] then a := a − 1 b := b + 1 il_in_10 := FALSE [New!] end 6 xxx_arr
ML_tl_green il_out_10 = FALSE inv3_16 inv3_16 : il_out_10 = TRUE ⇒ il_tl = green IL_tl_green il_tl green (ml_out_10 = FALSE) 2 inv3_16 ML_tl_green 2 7.4 4
FALSE “on” ENV-5 ML_out_dep
ML_in_arr when MLIN_SR = off ml_in_10 = FALSE C > 0 then MLIN_SR := on
IL out arr when
4
ENV-3 7.5 variant_3 : 12-( ML_OUT_SR+ML_IN_SR+IL_OUT_SR+IL_IN_SR+2*( ml_out_10+ml_in_10+il_out_10+ il_in_10)) variant_2 7.6 3