University of Nijmegen (THE NETHERLANDS)
Translation of PLC programs into compact timed automata
CADP (Construction and Analysis of Distributed Processes)
Programmable Logic Controllers (PLCs) are increasingly used for safety
critical applications in a variety of industrial settings. Therefore,
the formal verification of programs for PLC applications in considered
of most importance in order to ensure their reliability. Since many
of the processes that are controlled by PLCs are time critical, time
is considered to be an integral part of the control exerted by PLCs.
Timed automata (TA) appear as an appropriate formalism for modelling
and verifying PLC systems, because they allow to capture real-time
aspects. Moreover, a number of model-checking tools, such as UPPAAL,
KRONOS, and HYTECH are available for timed automata. One of the
problems encountered when verifying PLC applications is the state space
explosion. The work presented here aims to tackle this problem by
splitting the PLC systems into a timed and an untimed part and reducing
the state space of the latter by using the CADP toolset.
The first step in the approach is to translate a PLC program, written in the Instruction List (IL) language standardized by IEC, into a timed automaton accepted by UPPAAL. This is done by converting (a subset of) IL into an intermediate format, which is then translated into a TA. This intermediate format also serves as basis for state space reduction using CADP. For this purpose, a compiler was constructed that abstracts from timing and is able to produce a LOTOS specification describing the untimed part of a PLC program. The labelled transition system (LTS) of the resulting LOTOS specification is obtained using the CAESAR compiler and is minimized using the ALDEBARAN tool. The resulting LTS is translated back into a TA accepted as input by UPPAAL. This approach leads to substantial state space reductions, even for small examples.
The method of dissecting a PLC program into a timed and an untimed part
can be performed quite elegantly. The untimed part can be processed
using CADP, via a translation to LOTOS, in order to reduce the state
space. Since in most cases the untimed part is much larger than the
timed part, the reductions obtained in practice are substantial.
Further research concerns the experimentation with larger PLC programs
and the application of the approach for other languages from the IEC
standard, such as Structured Text (ST) and Sequential Function Chart
"Compact Timed Automata for PLC Programs".
Technical Report CSI-R9925, University of Nijmegen, November 1999.
Available on-line at: http://www.cs.kun.nl/csi/reports/info/CSI-R9925.html
or also from our FTP site in PDF or PostScript
Computing Science Institute
Faculty of Mathematics and Computer Science
University of Nijmegen
NL-6525 ED Nijmegen
Tel: +31-24-365 22 71
Fax: +31-24-365 31 37
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|