Abstract
Programmable Logic Controllers (PLC) are widespread in the manufacturing and processing industries to realize sequential procedures and to avoid safety-critical states. For the specification and the implementation of PLC programs, the graphical and hierarchical language Sequential Function Charts (SFC) is increasingly used in industry. To investigate the correctness of SFC programs with respect to a given set of requirements, this contribution advocates the use of formal verification. We present two different approaches to convert SFC programs algorithmically into automata models that are amenable to model checking. While the first approach translates untimed SFC into the input language of the tool Cadence SMV, the second converts timed SFC into timed automata which can be analyzed by the tool Uppaal. For different processing system examples, we illustrate the complete verification procedure consisting of controller specification, model transformation, integration of dynamic plant models, and identifying errors in the control program by model checking.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Lewis, R.: Programming industrial control systems using IEC 61131-3. IEE (1998)
International Electrotechnical Commission, Technical Committee No. 65: Programmable Controllers – Programming Languages, IEC 61131-3. (2003) Ed. 2.0
Moon, I., Powers, G.J., Burch, J.R., Clarke, E.M.: Automatic verification of sequential control systems using temporal logic. AIChE Journal 38, 67–75 (1992)
Kowalewski, S., Engell, S., Preussig, J., Stursberg, O.: Verification of logic controllers for continuous plants using timed condition/event system models. Automatica 35, 505–518 (1999)
Lampérière, S., Lesage, J.J.: Formal verification of the sequential part of PLC programs. In: Boel, R., Stremersch, G. (eds.) Discrete Event Systems, pp. 247–254. Kluwer Academic Publishers, Dordrecht (2000)
Bauer, N., Huuck, R.: Towards automatic verification of embedded control software. In: Proc. 2nd Asia-Pacific Conf. on Quality Software, pp. 561–567 (2001)
Clarke, E., Wing, J.: Formal methods: State of the art and future directions. ACM Computing Surveys 28, 626–643 (1996)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Fujino, K., Imafuku, K., Yamashita, Y., Nishitani, H.: Design and verification of the SFC program for sequential control. Comp. Chem. Eng. 24, 303–308 (2000)
L’Her, P., Scharbarg, J., Le Parc, P., Marce, L.: Proving sequential function chart programs using automata. In: Champarnaud, J.-M., Maurel, D., Ziadi, D. (eds.) WIA 1998. LNCS, vol. 1660, pp. 149–163. Springer, Heidelberg (1999)
Bornot, S., Huuck, R., Lakhnech, Y., Lukoschus, B.: Verification of sequential function charts using SMV. In: Proc. Int. Conf. on Parallel and Distributed Processing Techniques and Applications, pp. 2987–2993 (2000)
McMillan, K.: The SMV Language. Cadence Berkeley Labs (1999), http://wwwcad.eecs.berkeley.edu/kenmcmil/language.ps
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.: Symbolic model checking: 1020 states and beyond. Information and Comp. 98, 142–170 (1992)
Havelund, K., Larsen, K., Skou, A.: Formal verification of a power controller using the real-time model checker Uppaal2k. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 277–298. Springer, Heidelberg (1999)
Bauer, N., Huuck, R., Lukoschus, B., Engell, S.: A unifying semantics for sequential function charts. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 400–418. Springer, Heidelberg (2004)
Clarke, E., Emerson, E.: Synthesis of synchronisation skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–350. Springer, Heidelberg (1982)
Bauer, N., Kowalewski, S., Sand, G., Löhl, T.: A case study: Multi product batch plant for the demonstration of control and scheduling problems. In: Proc. Analysis and Design of Mixed Processes, pp. 383–388 (2000)
Larsen, K.G., Pettersson, P., Yi, W.: Compositional and Symbolic Model-Checking of Real-Time Systems. In: Proc. of the 16th IEEE Real-Time Systems Symposium, pp. 76–87. IEEE Computer Society Press, Los Alamitos (1995)
Behrmann, G., David, A., Larsen, K.G.: M ller, O., Pettersson, P., Yi, W.: Uppaal – present and future. In: Proc. of 40th IEEE Conference on Decision and Control, IEEE Computer Society Press, Los Alamitos (2001)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer 1, 134–152 (1997)
Aceto, L., Bergueno, A., Larsen, K.G.: Model Checking via Reachability Testing for Timed Automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 263–280. Springer, Heidelberg (1998)
Ehrig, H., Engels, G., Kreowski, H.J., Rozenberg, G.: Handbook of graph grammars and computing by graph transformation: applications, languages, and tools, vol. 2. World Scientific Publishing Co., Inc., Singapore (1999)
Stursberg, O.: Analysis of switched continuous systems based on discretization. In: Proc. 4th Int. Conf. on Automation of Mixed Processes, pp. 73–78 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bauer, N. et al. (2004). Verification of PLC Programs Given as Sequential Function Charts. In: Ehrig, H., et al. Integration of Software Specification Techniques for Applications in Engineering. Lecture Notes in Computer Science, vol 3147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27863-4_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-27863-4_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23135-6
Online ISBN: 978-3-540-27863-4
eBook Packages: Springer Book Archive