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

3

T T ( M +)

i := 0 i := 0

[ i ≤ 2] [ i< 3]

[ i> 2] [ i ≥ 3]

λ 11 λ 11

i := i +1 i := i +1

j := 0 j := 0

[ j ≤ 2] [ j< 3]

[ j> 2] [ j ≥ 3]

λ 12 λ 12

j := j +1 j := j +1

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

3

Fig. 9. T →T ( M +): I/O-equivalent guard transformation

Finally, a valuation-preserving change of guard conditions ([ i

≤ →

[ i< 3] , [ i>

2]

→

[ i

≥ T M

2] +) which completes the proof, as far as the code

fragments shown here for illustration purposes are concerned.

3] etc.) yields (

8Con lu on

In this paper we have given an overview of a complete model-driven development
and verification approach for railway and tram control systems. The approach
provides a framework consisting of

1. a domain-specific language,
2. a collection of tools, including (a) syntax and static semantics checkers for the
language, (b) generators producing executable models of the control system
and its physical environment as well as proof obligations, (c) a bounded
model checker and (d) an object code verifier,