Compact Timed Automata for PLC Programs
H.X. Willems · 1999
In this work a set of tools is developed to convert programs for Programmable Logic Controllers (PLCs) into timed automata in order to facilitate the verification of such programs. It is shown that our timed automata models of PLC programs can be dissected into a timed and an untimed part. Typically, the untimed part is much larger than the timed part and can be reduced in size by using the CADP toolset. The reduction in state space is substantial, even for small PLC programs. Keywords: Programmable Logic Controllers, PLC-Automata, Timed Automata AMS Subject Classification (1991): 68N20, 68Q05, 68Q55, 68Q60 CR Subject Classification (1994): C.3, D.2.4, D.2.5, D.3.2, D.3.4, F.3.1 Permanent address: Philips Research Laboratories, Prof. Holstlaan 4, 5656 AA Eindhoven, The Netherlands, [email protected] 1 1 Introduction Programmable Logic Controllers (PLCs) are increasingly used for safety critical applications in a variety of industrial settings. The purpose of the work ...