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

For performing real-time computations the cycle time of the PLC has to be taken
into account. Thus PLCs cannot react arbitrarily fast to changes of the sensor
values.
Developing a method for the design of correct real-time software for PLCs
has been a challenge for the author's research group. In the following sections
we describe the results achieved so far.

4 Requirements: Constraint Diagrams

When discussing and formalising the requirements of a system, application ex-
perts and computer science experts have to come to an agreement. The direct
use of logic is often claimed to be an obstacle for engineers. Therefore graphic
notations have been proposed for the specication of behavioural properties.
Most prominent are Message Sequence Charts (MSCs) developed for the area
of telecommunication [20,27]. In its original form MSCs describe only individual
typical communication traces of a reactive system. Various extensions of MSCs
are currently under development, e.g. to deal with real-time [2], but there is the
danger that these extensions lack the intuitive appeal of the original MSCs. For
the graphic description of temporal properties Symbolic Timing Diagrams have
been developed and successfully applied in several industrial projects [36,5].
To deal with real-time properties graphically, we use so-called Constraint Di-
agrams (abbr. CDs) [12,9]. A CD describes the timing behaviour of one or more
observables in the sense of Section 2 in an assumption-commitment style. For
each observable it displays a sequence of values, possibly annotated with time
intervals describing their duration. The time-wise relationship between the val-
ues of dierent observables is described by arrows connecting these values, again
possibly annotated with time intervals. Both observation values and time inter-
vals can be surrounded by boxes. Whereas normal values and intervals represent
assumptions, boxed values and intervals represent commitments. Semantically,
a CD represents a logic implication of the form

assumptions ) commitments:

We introduce CDs by way of an example.

Example 1. A watchdog is a real-time system for continuously checking an input
signal

S S A

should be
raised within 1 second. To model this system we consider two Boolean observ-
ables:

.If has been absent for more than 10 seconds an alarm

S : Time −! f 0 ; 1 g

A : Time −! f 0 ; 1 g :

The behavioural requirements for these two observables can be specied by the
following CD: