Microsoft word - v173_web.doc

Formalization of existing PLC Programs: A Survey
Juniorprofessorship Agentenbased Automation
Abstract: In recent years, the interest in the formal-
ization of PLC programs increased. The paper pro-
vides a classification scheme for the works done in
this field. This scheme includes the sources used for
formalization, the level of the formalization process
(i.e. the complexity of structures that could be han-
dled by the approach), the aim of the formalization
(Re-Engineering or Verification) and the formal
model used to represent the formalized PLC pro-
gram. The scheme is applied to several examples.
Figure 1: Reasons for Formalization of PLC Programs.
Programmable Logic Controllers (PLCs) are a special type of computers that are used in industrial and safety- The process of formalization of already implemented critical applications. The purpose of a PLC is to control PLC code is also known as reinterpretation [1] or as a particular process, or a collection of processes, by translation of the PLC program form one source to an- producing electrical control signals in response to elec- other (formal language or programming language) [2]. Due to the broadness of the field with practitioners and The systems controlled by PLCs vary tremendously, academics from different specialized areas working in with applications in manufacturing, chemical process it, this Survey cannot be complete in any sense. How- control, machining, transportation, power distribution, ever considerable effort was made to give a concise and many other fields. Automation applications can overview. The paper provides a classification scheme range in complexity from a simple panel i.e. to operate for the works done in formalization of PLC programs the lights in a conference room to completely automated and applies this scheme to several examples. production systems like e.g. a brewery in which the ma-chinery for everything – from dispensing and mixing The paper is structured as follows: in Section II the ingredients to controlling the brewing process and even classification scheme is introduced. The four sections filling and sealing of bottles – is under PLC control. following (III to VI) discuss the four classification crite-ria in detail. Section VII presents a list of examples and There are two main reasons for the formalization of classifies them according to the presented criteria. PLC programs (cf. Fig. 1). The first is the need for for-mal Verification and Validation, Simulation and Analy- sis of existing systems due to increased awareness of safety and quality. The second is the constant progress Research on the formalization of PLC programs can be involved in production and its automation. This means classified according to four main criteria: that existing programs have to be changed in order to meet new production demands or have to be transferred • The sources used for the formalization, which are to new controller hardware (re-implementation). Since o the language the PLC program is written in in most cases there is no formal description of the pro-grams available that could be used for these tasks, this o and – if applicable – the additional information description has to be generated from the existing code. The only other solution would be to do a completely • The level of the formalization of the PLC based on the complexity of structures that the formalization process could handle (simple algorithm, complete Bani Younis, M.; Frey, G.: Formalization of Existing PLC Programs: A Survey. Proceedings of CESA 2003, Lille (France), Paper No. S2-R-00-0239, July , 2003. program, or even complete configuration contain- When trying to formalize a given program on a higher level of abstraction, i.e. not line by line but by identify-ing useful structures. The know-how of expert pro- • The aim of the formalization, i.e. which methods grammers can be used in this identification process. should be applied to the generated formal model This know-how is either applied directly or transferred to a database for the use of non-specialists. • The formal model used to describe the PLC pro- The approaches applied on the formalization of the PLC programs vary in their range in three different classes. • The formalization of parts of the control pro-
gram (algorithms): There are approaches that are
For many years, in the area of PLC control there have suitable for the formalization of algorithms but not been only proprietary programming languages used to of complete programs because they have no means program one special PLC of one special vendor. How- for describing all the necessary language elements ever, in 1993 the International Electrotechnical Com- of the PLC. These approaches are especially useful mission (IEC) published the IEC 61131 International if a specific function of a controller has to be tested Standard for Programmable Controllers [3]. Part 3 of this standard defines a suite of five programming lan-guages that are used increasingly often instead of the • The formalization of complete programs: In this
proprietary languages. In the standard there are two tex- class a model of the behavior of the program is de- tual languages: Instruction List (IL) and Structured Text rived. Most work done in the area of the formal (ST), and two graphical languages: Ladder Diagram methods and formalization of PLC is in this class. (LD) and Function Block Diagram (FBD). A fifth lan- After finishing the model it can be tested using dif- guage, the graphical or textual Sequential Function ferent test methods of verification and validation. Chart (SFC) is proposed to define the structure of a The tested and optimized program can be re- implemented on the original source system or on a Ladder Diagram has its roots in the USA. It is based on the graphical presentation of Relay Ladder Logic. Instruction List is its European counterpart. As textual • The formalization of the whole control configu-
rations: Complete configuration of a control sys-
Function Block Diagram is very common to the process tem consisting of several PLC programs on one or industry. It expresses the behavior of a controller as a more PLCs. This approach is important for the re- set of interconnected graphical blocks, like in electronic implementation of control system software on new Structured Text is a very powerful high-level language that is close to Pascal. The fifth language is the Sequential Function Chart (SFC). SFC elements are defined for structuring the in- Two main important fields for the formalization of PLC ternal organization of programmable controller pro- programs have been growing up in the recent time: Re- verse-Engineering and Verification and Validation. In some formalization approaches in addition to the Re-implementation or Reverse Engineering is a process code of the controller information about the plant or ex- of evaluating something to understand how it works in Additional information about the control plant is There is a constant need for updating and renovating needed, if in V&V properties of the controlled plant business-critical software systems for many and diverse should be tested. The system environment or the con- reasons: business requirements change, technological trolled system is modeled and is verified together with infrastructure is modernized, the government changes the model of the program. The model of the system un- laws etc. Therefore, in the area of software engineering der control can also be used in simulation. Knowledge the subjects of reverse engineering and system renova- about the physical structure of the plant is especially tion become more and more important. The interest in useful in re-interpretation of the controller. such subjects originates from the difficulties that are model defined by the system and check whether the encountered when attempting to maintain extremely large software systems. Such software systems are often called legacy systems, since it is a legacy of many dif- Theorem proving proves that an implementation satis- ferent people that have developed and maintained them. fies a specification by mathematical reasoning. Imple- It is not hard to understand that it is very difficult – if mentation and specification are expressed as formulas not impossible – to maintain them. The reverse engi- in a formal logic. The required relationship (logical neering of PLC programs is required, as there is often equivalence/logical implication) described as a theorem no documentation for the implemented system. has to be proven within the context of a proof calculus. The proof system is a set of axioms and inference rules Program transformations have been advocated as a (simplification, rewriting, induction, etc.) method for accomplishing reverse engineering. The hy-pothesis is that the original source code can be progres- sively transformed into alternative forms, but with the same semantics. At the end of the process, an equivalent The following formalisms are among the important for- program is acquired, but one which is much easier to • Automata: automata and also timed or hybrid
automata are used in the verification of PLCs. For more information on hybrid automata see [6]. The second aim of formalization is Verification and Validation (commonly referred to as V&V) of the PLC • Petri nets: different types of Petri nets are used as
program. In recent years the interest for analyzing PLC programs has increased to help in deciding if the pro-gram verifies specifications like safety, liveness and There are also other formalisms like Condition/Event timing properties. In [4] an example is given that shows systems known as C/E, Higher Order Logic, Synchro- how V&V can help improving a controller. V&V is nous Languages, and General Transition Systems. concerned with answering two fundamental questions. Speaking broadly, validation is concerned with building the right product, and verification is concerned with In the following, examples are listed and categorized V&V techniques can be applied throughout the product according to the Target of formalization. lifecycle to help assure that the correct product is being built and that the product is being built correctly. Two A. Reverse Engineering or Re-implementation levels of research are done on the verification of PLC programs: verification of the program with a model of • In [7] an automatic re-documentation, reformatting the plant or the environment, or the verification of the and transformation of IL programs into a hypertext program with respect to the control specification. on the basis of HTML is given. This method is in-tended for Software-visualization, static analysis, To make analytic techniques computationally tractable, abstract models in the language used by the analytic tools must be generated from the specifications, code, • A Reverse Engineering method for the conversion and models. Currently, the generation of these abstract into a control description with state diagrams is models is both a practical and theoretical bottleneck in given in [8]. These state diagrams are formatted ac- cording to a functional hierarchic structure. The source here is IL and additional information about There is a variety of V&V methods (e.g. static analysis, abstract interpretation, runtime verification automated abstraction, invariant generation, slicing). However the • In [9] FBD from a source system is translated and two most promising formal methods used in V&V so re-implemented to transfer a complete controller far are model checking and theorem proving. configuration to a new control system (known as migration of process control system software). Model checking is a method for formally verifying fi- Here the know-how of programmers is important nite-state concurrent systems. Specifications about the for the translation. In the approach the translation is system are expressed as temporal logic formulas, and not based on single FBD elements but on the iden- efficient symbolic algorithms are used to traverse the tification of functional structures (e.g. a set of con-nected FBD elements describing some function). To identify these structures the know-how of the run-time errors and provides information about the programmers is used to build a data-base contain- program structure, this method checks for dead ing functional structures of the source system and corresponding structures of the target system. • A method for translating an IL program into a tran- sition system is presented in [19]. LTL is used to write behavioral properties of the controlled system These examples are further classified according to the and coding of the operational semantics into SMV language the original PLC program is written in: that is used for the check for properties. • In [20] programs in IL are modeled as Petri nets. The model of the program is then composed with • In [10] the variables as well as the different con- Petri net models of the process into one model of structs of the ST language are modeled using com- the controlled system. The properties to be verified municating automata. There are automaton models are expressed in CTL and the SMV model checker for the while, for, if then else, and negation con-
structs. The automata of the used variables and of the constructs are composed to express the ST blocks. The resulting model tends to be very large. This technique has been used to translate ST pro- • The aim of [21] is an effective translation of the grams into input code for the model-checker Ca- SFC syntax into SMV [22] model checking source dence SMV. Each component is defined as a mod- code. Using SMV the SFC is verified for reachabil- ity properties, causal dependencies between the in-put variables and reachability. • In [23] a timed automaton of the plant or the con- • In [11] a model is given for instruction list. The trolled system is built. The PLC program written in structure of the PLC, the program logic, the process SFC is translated by creating a discrete transition inputs, and the process outputs are modeled using system for the logic part and introducing a clock Condition/Event systems [12]. The Model-Checker variable for each timer. After that composition of VERDICT [13] is used to verify the properties of the timed automata of the plant and the controller the composition of the models together with the model the valid ranges of the clock variables are • In [14] automata are used to model PLC algorithms • A method to convert SFC to a Hybrid Automata that are programmed in a sub-set of IL. Timers of System (HAS) is given in [25]. The process under type TON are also modeled as timed automata. control is also modeled as a Hybrid Automata Sys- Complex language elements such as function and tem. Both models are then synchronized and then function block calls are not considered. The formal- an algorithmic solution to the reachability problem ization is restricted to Boolean variables. A tool of the combined HAS description is applied. was developed based on this work described in [15]. This tool translates programs written in IL to • The work of [26] was carried out as a part of a case timed automaton. Variables of type integer in this study for the EC VHS (verification of Hybrid Sys- model are also allowed. The conversion of the IL tems) [27]. The goal of this work is to verify and program to the models is divided to timed automata design a PLC program for an experimental chemi- and un-timed automata (which is in general larger cal Plant. Promela/SPIN [28] is used for the verifi- than the timed part). The un-timed part is mini- cation of the PLC program and to derive time opti- mized using the toolset Caesar/Aldebaran Devel- mal schedules with reasonable time and space re- opment Package [16]. Information about the system environment is needed and can be modeled using a timed automata synchronized with a model of the • Further works on the verification and validation of PLC program as an interface to the input and out- put variables. To verify the model the UPPAAL model checker is used [17]. • Static analysis is applied to programs written in IL • In [30] an approach for the automated verification in [18]. An abstract interpretation algorithm is pre- of LD and timed function blocks (of type TON) is sented which allows static checking for possible presented. The algorithms are translated into state automata The SMV as symbolic model checker is cording to the target and the model used for this formal- • Translation of LD programs into Complementary- One reason for the restriction of formalization ap- Places Petri Nets [32], [33] is performed in [31]. proaches to single programs or algorithms is the prob- This type of PN contains an annotation for a couple lem of getting the project information from a PLC pro- of places associated to the values for the token (true gramming tool. At the moment there are only vendor or false) and for the modeling of Boolean variables. specific formats. However, recently the PLCopen – a The LD operators are modeled by a PN type struc- PLC user organization (see http://www.plcopen.org) – ture and the whole specification of the LD is then started a Technical Committee to define an XML based format for projects according to IEC 61131-3. This new format will ease the access of formalization tools to all • In [34] a toolset called PLCTOOLS has been intro- duced. The FBD programs are modeled and are de- scribed as High Level Timed Petri Nets (HLTPN) [1] G. Frey and L. Litz: Formal methods in PLC programming. [35]. HLTPN are used for validating the design and Proc. of the IEEE Conf. on Systems, Man and Cybernetics generating the code. MATLAB / S1MULINK pro- (SMC'2000), Nashville, USA, Oct. 2000, pp. 2431-2436. vides suitable means for specifying and simulating [2] S. Lampérière-Couffin, O. Rossi, J.-M. Roussel, J.-J.Lesage: the plant. This work can be considered also as Re- Formal Validation of PLC Programs: A SURVEY. Proc. of the engineering method since from the FBD and using European Control Conference (ECC99), Karlsruhe, Germany, Sept. 1999, paper N° 741. this tool a code in C++ of the FBD program can be [3] International Electrotechnical Commission. IEC International generated and the reuse of the existing software on Standard 1131-3, Programmable Controllers, Part 3, Program- [4] O. De Smet, S. Couffin, O. Rossi, G. Canet, J.-J. Lesage, Ph. • Controllers defined according to IEC 61499 [36] Schnoebelen, H. Papini: Safe programming of PLC using formal are formalized in [36]. The controller code is in verification methods. Proc. 4th Int. PLCopen Conf. on Industrial Control Programming (ICP'2000), Utrecht, the Netherlands, Oct. FBD format and the overall system is organized in IEC 61499 Function Blocks. These Blocks contain [5] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill und L.J. Execution Control Charts (ECC), which are state Hwang: Symbolic Model Checking: 10 20 States and Beyond. In- machines connecting event inputs with algorithms formation and Computation, 98: pp. 142-170, 1992. and event outputs. In the approach this complete [6] T. A. Henzinger: The Theory of Hybrid Automata, Proc. of the structure is automatically translated to Signal-Net 11th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, July 1996, pp. 278-292. Systems (SMS). The tool VEDA allows the model- [7] R .Kliewer: Reverse Engineering von Steuerungssoftware. Ph.D. ing of the controlled plant and the controller by thesis, University of Kaiserslautern, Germany, Institute for Pro- means of Signal-Net Systems [38]. On the com- bined model of plant and controller model- [8] A. Storr und S. Kraneis: Restrukturierung und Reverse Enginee- checking is performed using SESA [39] (Sig- ring von SPS- Programmen. Fachtagung Entwurf komplexer nal/Event system analyzer) – a powerful model- Automatisierungssysteme (EKA'97), Braunschweig, 1997, pp. 446-461. [9] Fay, A.: Methoden zur Unterstützung der Migration von Pro- zessleitsystem-Software.T.A. atp 44, Heft 6 2002, pp. 39-44. [10] G. Canet: Vérification des programmes écrits dans les langages de programmation IL et ST définis par la norme IEC 61131-3. Table 1 summarizes the examples according to the crite- Thèse ENS de Cachan, December 2001. ria discussed in the last sections. It has to be mentioned [11] H. Treseler, N. Bauer, S. Kowalewski: Model-Checking von that – besides all efforts – there is no method at the AWL-Programmen. Lambda. Technischer Bericht, 10. Februar 2000, gekürzte Version in Fachtagung Verteilte Automatisie- moment that is capable of the automatic formalization rung, Magdeburg, 22./23. März 2000, pp 286-293. of complete PLC projects according to IEC 61131-3. [12] R.S. Sreenivas and B.H. Krogh: On Condition/Event Systems with Discrete State Realizations. Discrete Event Dynamic Sys-tems: Theory and Applications, Kluwer Academic Publishers, [13] S. Kowalewski, N. Bauer, J. Preußig, O. Strusberg, and H. Tre- Our interest was to present different approaches to for- seler: An environment for model-checking of logic control sys- malize PLC programs and to give examples on this tems with hybrid dynamics. In Proc. IEEE int symp. On Com-puter Aided Control System Design, 1999, pp 97-102. field. These works are categorized in four criteria: ac- [14] A. Mader , H. Wupper: Timed Automaton Models for Simple cording to the source in which the program is written in, PLC. Proc. of the Euromicro Conference on Real-Time Systems according to the level of formalization – the whole pro- 1999, IEEE Computer Society Press, June 1999, pp. 114-122. gram or only part of it – is needed to be formalized, ac- [15] H. X. Willems: Compact timed Automata for PLC Programs. [29] J.-M Roussel and J.-J. Lesage: Validation and Verification of Technical Report CSI-R9925, University of Nijmegen, Novem- grafcets using finite state machine. Proc. of the IMACS-IEEE Multiconference on Computational Engineering in Systems Ap- [16] CADP home-page: http://www.inrialpes.fr/vasy/cadp/. plications (CESA'96), Lille, France, July 1996, pp. 758-764. [17] UPPAAL home-page: http://www.uppaal.com/. [30] O. Rossi, Ph. Schnoebelen: Formal Modelling of Timed Function Blocks for the Automatic Verification of Ladder Diagram Pro- [18] S. Bornot, R. Huuck, B. Lukoschus, Y. Lakhnech: Utilizing grams. Proc. 4th Int. Conf. Automation of Mixed Processes: Hy- Static Analysis for Programmable Logic Controllers. Proc. of the brid Dynamic Systems (ADPM), Dortmund, Germany, Sept. 4th International Conference on Automation of Mixed Processes 2000, Shaker Verlag, Aachen, Germany, 2000, pp.177-182. (ADPM), Dortmund, Germany, Sept. 2000, pp. 183-187. [31] I. Hatono, K. Baba, M. Umano, H. Tamura: Automatic Genera- [19] G. Canet, S. Couffin, J.-J. Lesage, A. Petit and Ph. Schnoebelen. tion of Fault Detection Models for Programmable Controller- Towards the automatic verification of PLC programs written in Based Manufacturing Systems Using Complementary-Places Instruction List. Proc. of the IEEE Conf. on Systems, Man and Petri Nets., IFAC World Congress 1996. Cybernetics (SMC), Nashville, USA, Oct. 2000, pp. 2449-2454. [32] S. Christensen, and N.D. Hansen: Coloured Petri Nets Extended [20] T. Mertke, T. Menzel: Methods and tools to the verification of with Place Capacities Test Arcs and Inhibitor Arcs. Proceedings safety-related control software, IEEE International Conference of 14th International Conference on Application and Theory of on Systems, Man and Cybernetics, (SMC), Nashville, USA, Oct. Petri Nets, Chicago, USA, Springer-Verlag 1993, pp. 186-205 [33] C. Lakos, S. Christensen: A General Systematic Approach to Arc [21] S. Bornot, R. Huuck, B. Lukoschus, Y. Lakhnech: Verification of Extensions for Coloured Petri Nets. Proc. of the 15th Interna- Sequential Function Charts using SMV. Proc. of the International tional Conference on Application and Theory of Petri Nets, Conference on Parallel and Distributed Processing Techniques Zaragoza, Spain, 1994, Springer-Verlag, pp. 338-357. and Applications (PDPTA 2000), Las Vegas, USA, June 2000, Vol. V, pp. 2987-2993. [34] L. Baresi, M. Mauri, A. Monti, and M. Pezze. PLCTools: De- sign, Formal Validation, and Code Generation for Programma- [22] K.L. McMillan. The SMV system. Carnegie-Mellon University, ble Controllers. Proc. of the IEEE Conference on Systems, Man, February 1992. Draft version describing SMV revision 2.2. and Cybernetics (SMC), Nashville, USA, Oct. 2000, pp. 2437- [23] S. Kowalewski, S. Engell, R. Huuck, Y. Lakhnech, B. Lu- koschus, and L. Urbina: Using Model-Checking for Timed Auto- [35] Ghezzi, D. Mandrioli, S. Morasca, and M. Pezzè: A Unified mata to Parameterize Logic Control Programs. 8th European High-Level Petri Net Model for Time-Critical Systems. IEEE Symposium on Computer Aided Engineering, Brugge, Belgium, Transactions on Software Engineering, 17(2): Feb. 1991, pp 160- [24] Henzinger, T.H., Ho, P.H., Wong-Toi, H. (1997) A User guide to [36] Function Blocks for Industrial Process Measurement and Control HyTech. http://www-cad.eecs.berkeley.edu/~tah/HyTech/ Systems International Electrotechnical Commission, Tech. [25] G. Hassapis, I. Kotini, Z. Doulgeri: Validation of a SFC soft- Comm. 65, Working group 6, Committee draft. ware specification by using Hybrid Automata.Proc. of the 9th [37] V. Vyatkin, H.-M. Hanisch: Modelling of IEC 61499 function Symposium on INformation COntrol in Manufacturing blocks - a clue to their verification. Proc. of the XI Workshop on INCOM'98, Nancy-Metz, France, June 1998, Vol. II, pp. 65-70. Supervising and Diagnostics of Machining Systems, Karpacz, [26] Ed. Brinksma and A. Mader: Verification and optimization of a Poland, March 12-17, 2000, pp. 59 – 68. PLC control Schedule. Int. Journal on Software Tools for Tech- [38] P. Starke: Symmetries of signal-net systems. Workshop on Con- nology Transfer, 4 (1), 2000, pp. 21-33. currency, Specification and Programming, October 2000, pp. [27] A. Mader, E. Brinksma, H. Wupper, and N. Bauer: Design of a plc control program for a batch plant, VHS case study 1. Euro- [39] P. H. Starke and S. Roch: Analysing Signal-Net systems. Report, pean Journal of Control, 7 (4), 2001, pp. 416-439. Humboldt University Berlin, Institut für Informatik, Aug. 2000. [28] G.J. Holzmann: The model checker spin. IEEE Trans. on Soft- ware Eng., 23(5): May 1997, pp. 279- 295. berlin.de/lehrstuehle/automaten/tools/#sesa. Table 1: Classification of the Examples
Classification
Level Aim
Reference
Language Additional
Information
Programmers Know-How in database Configuration Re-Engineering Without additional information Program Verification Without additional information Algorithm Verification Timed Without additional information Program Verification No Without additional information Program Verification Automata Without additional information Program Verification Automaton Without additional information Algorithm

Source: http://www.aut.uni-saarland.de/uploads/media/GF_MBY_CESA_jul_2003.pdf