Correct Real-Time Software for Programmable Logic Controllers - Correct System Design: Recent Insights and Advances - page 332

expresses that prog correctly implements spec . By the transitivity of V we can

deduce prog req from the above two facts, i.e. prog correctly implements the

requirement .

This picture gets more complicated if the predicates associated with

req

term 1

and term 2 involve dierent observables, say term 1 involves more concrete ob-

c term 2 more abstract ones

servables and a . Then we need a linking invariant

a c

that relates the values of . Such an invariant is known from data rene-

ment [33]; it can also be expressed as a predicate, say

and

link a;c . Then correctness

becomes

term 1 ^ link a;c V term 2 ;

i.e. the conjunction of term 2 .

At this point one may argue that working with logical formulae expressing
the semantics of complex objects like requirements, specications and programs
is not practical. Here our approach is to keep the logic as much as possible in the
background, i.e. to use rules and algorithms that are based on the logic in order
to guarantee their correctness but to avoid exhibiting all details of the logic to
the users of the method. In the following we shall instantiate this approach by
particular choices for the levels of requirements, specications and programs,
and for the logic.

term 1 and link a;c has to imply

3 CaseStudy:TramControl

In this paper we look at an application area motivated by the UniForM project
that was performed jointly with the University of Bremen and the industrial
partner Elpro in Berlin. The project was concerned with a tool supported combi-
nation of formal methods for the development of correct software for distributed,
communicating and time-critical systems [23].
More specically, Elpro is engaged in the application domain of railway con-
trol. As a case study the safe control of a single track segment for trams (SCS)
was chosen (see Fig. 2). Single track segments represent possible dangerous sit-
uations that occur for example in the event of repair work.
The task of the SCS is to safely guide trams driving in opposite directions
through a single track segment so that no collision can occur on this segment. To
this end, suitable sensors and trac lights are installed along the track. For each
direction

i 2f 1 ; 2 g of the trams there are three sensors called ES i (entry sensor),

CS (leave sensor) as shown in Fig. 2. From the values

of these sensors the control under development has to compute the signals for
the trac lights of both directions. For each direction there are three possible
signals: Go, Stop and Ack , an acknowledgement for the tram drivers requesting
to pass the single track segment. There are several informal requirements that
the SCS should satisfy.

i (critical sensor) and LS i

Safety. No collision should occur on the single track segment, i.e. this critical
segment should be used in mutual exclusion .