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 the CADP Web 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

Back to the CADP research tools page