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

Correct Real-Time Software for
Programmable Logic Controllers ?

Ernst-Rudiger Olderog

Fachbereich Informatik, Universitat Oldenburg
Postfach 2503, D-26111 Oldenburg
Germany
E-mail: [e-mail]

Abstract. We present an approach to the design of correct real-time
software for Programmable Logic Controllers (PLCs), a widespread hard-
ware platform in the area of trac and automation control [19,26].
Requirements are formulated in a graphical formalism called Constraint
Diagrams (CDs) [12]. A CD consists of waveforms that describe the time-
wise behaviour of observables and of arrows that describe the timed in-
terdependencies between these waveforms. Design specications are for-
mulated as so-called PLC-Automata [7]. These can be understood as a
special class of timed automata that model in an abstract way the cyclic
behaviour of PLCs. Programs are formulated in ST (Structured Text), a
dedicated programming language for PLCs. PLC-Automata can be easily
compiled into ST code.
The semantic link between CDs and PLC-Automata is stated in terms
of the Duration Calculus [37], a logic and calculus for specifying real-
time behaviour. This enables us to formally establish the correctness of
designs with respect to the requirements.
The approach is illustrated by a case study dened by an industrial part-
ner engaged in designing railway signalling systems [23]. It is supported
by a tool called Moby/plc [11].

1 Introduction

Real-time systems are reactive systems where reactions to certain inputs have to
occur within given time intervals [14,24,21,22,18]. These systems usually consist
of some physical process for which a suitable controller has to be constructed such
that the controlled process exhibits the desired time dependent behaviour. The
interaction between process and controller proceeds via sensors and actuators
as shown in Fig. 1. When constructing the controller the reaction times of all
components of this system have to be taken into account.
The design of a real-time controller typically involves several levels of ab-
straction, in particular the levels of
? This work was partially funded by the German Ministry for Education and Research
(BMBF), project UniForM, grant FKZ 01 IS 521 B3, and the Leibniz Programme
of the German Research Council (DFG) under grant Ol 98/1-1.