Database of Research Tools Developed Using CADP

Timed Automata for Programmable Logic Controllers

Organisation: University of Nijmegen (THE NETHERLANDS)

Functionality: Translation of PLC programs into compact timed automata

Tools used: CADP (Construction and Analysis of Distributed Processes)

Period: 1999

Description: 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.

Conclusions: 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 (SFC).

Publications: [Willems-99] H.X. Willems. "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
Contact:
Angelika Mader
Computing Science Institute
Faculty of Mathematics and Computer Science
University of Nijmegen
Toernooiveld 1
NL-6525 ED Nijmegen
The Netherlands
Tel: +31-24-365 22 71
Fax: +31-24-365 31 37
E-mail: mader@cs.kun.nl



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page