Abstract
Programmable logic controllers (PLC) are widely used in industries ranging from assembly lines, power plants, chemical processes to mining and rail automation. Such systems usually exhibit high safety requirements, and downtimes due to software errors entail intolerably high economic costs. Hence, their control programs are particularly suited for applying formal methods; in particular, bounded model checking (BMC) techniques based on satisfiability modulo theories promise to be highly beneficial in this domain.
In this paper, we investigate adaptations and extensions of property dependent static analyses which operate on a novel form of intermediate code and which are tailored specifically to model checking PLC programs. In our experiments, our program transformations drastically reduce the size of formulae for BMC and speed up the verification times by orders of magnitude.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Frey, G., Litz, L.: Formal methods in PLC programming. In: Systems, Man, and Cybernetics, vol. 4, pp. 2431–2436. IEEE Computer Society (2000)
Younis, M.B., Frey, G.: Formalization of existing PLC programs: A survey. In: CESA, pp. 234–239 (2003)
Fokkink, W., Hollingshead, P.: Verification of interlockings: From control tables to ladder logic diagrams. In: FMICS, pp. 171–185 (1998)
Groote, J.F., Warners, J.P.: The propositional formula checker HeerHugo. Journal of Automated Reasoning 24(1-2), 101–125 (2000)
Kanso, K., Moller, F., Setzer, A.: Automated verification of signalling principles in railway interlocking systems. ENTCS 250(2), 19–31 (2009)
Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of PLC programs written in Instruction List. In: 2000 IEEE Int. Conf. on Systems, Man, and Cybernetics, pp. 2449–2454. IEEE (2000)
Meulen, M.: Verification of PLC source code using propositional logic. Master’s thesis, Technical university of Eindhoven (2010)
Pavlovic, O., Pinger, R., Kollmann, M.: Automation of formal verification of PLC programs written in IL. In: Verification Workshop. CEUR Workshop Proceedings, vol. 259 (2007)
Loeis, K., Younis, M.B., Frey, G.: Application of symbolic and bounded model checking to the verification of logic control systems. In: ETFA, pp. 247–250 (2005)
Pavlovic, O., Ehrich, H.D.: Model checking PLC software written in function block diagram. In: ICST, pp. 439–448 (2010)
Sülflow, A., Drechsler, R.: Verification of PLC programs using formal proof techniques. In: FORMS/FORMAT, pp. 43–50 (2008)
Blech, J.O., Biha, S.O.: Verification of PLC properties based on formal semantics in Coq. In: SEFM. Volume 7041 of LNCS., Springer (2011) 58–73
Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD 2009, pp. 25–32. IEEE (2009)
John, K., Tiegelkamp, M.: IEC 61131-3: Programming Industrial Automation Systems. Springer (2010)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (1999)
Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann (1997)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD, pp. 173–180. IEEE (2007)
Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)
Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Lange, T., Neuhäußer, M.R., Noll, T. (2013). Speeding Up the Safety Verification of Programmable Logic Controller Code. In: Bertacco, V., Legay, A. (eds) Hardware and Software: Verification and Testing. HVC 2013. Lecture Notes in Computer Science, vol 8244. Springer, Cham. https://doi.org/10.1007/978-3-319-03077-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-03077-7_4
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03076-0
Online ISBN: 978-3-319-03077-7
eBook Packages: Computer ScienceComputer Science (R0)