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

1

T

.
. .

S 11

.L104

i := 0 edx := i

eax := i

.L103

eax := i

eax := reqsigNext [ eax ]

( ZF,SF ):=

reqsig [ edx ]:= eax

(2 = eax, 2 >eax )

i := eax

[ ZF ∨ SF ]

[ ¬ ( ZF ∨ SF )]

.
. .

.

.L104

eax := eax +1

S 11

j := 0

.

eax := i

.
. .

S 12

.L106

.L107

eax := j

edx := j

( ZF,SF ):=

eax := j

(2 = eax,
2 >eax )

j := eax [ ZF ∨ SF ]

eax := reqptNext [ eax ]

[ ¬ ( ZF ∨ SF )]

.
. .

.L107

eax := eax +1

S 12

reqpt [ edx ]:= eax

.

eax := j

.

1 associated with A after renaming of variables

Fig. 7. IOTS T

Now the mechanised equivalence proof is constructed as follows: (1) the be-
havioural IOTS model is constructed by using the semantic rules

for assembler instructions. After changing the names of assembler variables to
C-style notation according to mapping α M explained above, this results in an
IOTS

T ( A )of A

1 which is depicted in Fig. 7. (2) Applying the transformation rule shown

T