A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems - Formal Methods and Hybrid Real-Time Systems - page 343

2

T

i := 0

.L103

eax := i

( ZF,SF ):=

(2 = eax, 2 >eax )

i := eax

[ ZF ∨ SF ]

[ ¬ ( ZF ∨ SF )]

.L104

λ 11

eax := eax +1

j := 0

eax := i

.L106

eax := j

( ZF,SF ):=

(2 = eax, 2 >eax )

j := eax [ ZF ∨ SF ]

[ ¬ ( ZF ∨ SF )]

.L107

λ 12

eax := eax +1

eax := j

λ 11 = def reqsig [ i ]:= reqsigNext [ i ]
λ 12 = def reqpt [ j ]:= reqptNext [ j ]

1 2 : I/O-equivalent transformation

Fig. 8. T →T

1

in Fig. 6 to the regions S 11 and S 12 of T resultsisanI/O-equivalentIOTS

2

T depicted in Fig. 8. (3) Twofold application of other transformation rules

2 results in I/O-equivalent IOTS 3 shown on the left-hand side of Fig. 9.

on T T