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

method aims at Programmable Logic Controllers (PLCs) because they are simple
devices that are widespread in automation and trac technology [19,26].
A PLC interacts with sensors and actuators in a cyclic manner. Each cycle
consists of three phases: an input phase where sensor values are read and stored
in local variables, a state transformation phase where all local variables are
updated according to the stored program, and an output phase where the values
of some of the local variables are output to the actuators. Real-time constraints
can be implemented on PLCs with the help of timers that can be set and reset
during the state transformation phase. Also the cycle time of the PLC has to be
taken into account.
Design specications will abstract from most of the details of PLCs but
keep the concepts of timers and cycle time. In order to be understandable to
engineers they should also have a graphic representation. Most popular are state-
transition models. Finite state machines or automata are well understood since
the early days of computing and come with a graphic representation that appeals
to engineers. This model has been extended in several ways: Petri nets allow an
explicit representation of concurrency [32], state charts do this as well but also
add a concept of hierarchy [16], action systems allow to overcome the limitations
of a nite control state space [3], timed automata allow to model time by adding
explicit clocks [1].
We use an automata model with states and transitions suitably extended with
concepts of time and hierarchy. These automata are called PLC-Automata [7]
and can be understood as a variant of timed automata geared towards modelling
the PLC behaviour. We introduce PLC-automata by way of an example.

Example 2. Fig. 5 displays a PLC-Automaton serving as a design specication
for the lter FES . It consists of three states and reacts to inputs

tr; no tr and

Error . Inputs mark the transitions and outputs

appear inside the states. In the initial state (marked by an in-going arc) the
automaton outputs

by outputting N; T and X

N (no train) and stays in this state as long as the input

is no train . Once an input tr is detected, the automaton switches to the state

where the output is (train). In case an input Error is detected, the automa-

ton switches to the state where the output is

T

X (exception). In this state the

automaton stays under all possible inputs.
As for real PLCs, the real-time behaviour of a PLC-Automaton is determined
by an additional parameter, the cycle time " PLC , i.e. the upper bound for the

duration of one cycle. Since the input values are read only at the beginning
of each cycle, it takes up to

" PLC seconds for a PLC-Automaton to detect a
new input value provided this value is stable for that period of time. Glitches
of input values may not be detected by a PLC-Automaton. Then it takes up
to " PLC seconds for a PLC-Automaton to react to this new input. Thus in the

worst case it takes up to 2

" PLC seconds for a PLC-Automaton to react to a

new input value.
Additionally, explicit timing inscriptions can appear in the lower parts of
states. In this example we see that the states with output N and X have the

inscriptions 0 s and all . This species that in these states the automaton should