Abstract
Formal verification has become a recommended practice in the safety-critical application areas. However, due to the complexity of practical control and safety systems, the state space explosion often prevents the use of formal analysis. In this paper we extend our former verification methodology with effective property preserving reduction techniques. For this purpose we developed general rule-based reductions and a customized version of the Cone of Influence (COI) reduction. Using these methods, the verification of complex requirements formalised with temporal logics (e.g. CTL, LTL) can be orders of magnitude faster. We use the NuSMV model checker on a real-life PLC program from CERN to demonstrate the performance of our reduction techniques.
Chapter PDF
Similar content being viewed by others
References
Darvas, D., Fernández, B., Blanco, E.: Transforming PLC programs into formal models for verification purposes. Internal note, CERN (2013), http://cds.cern.ch/record/1629275/files/CERN-ACC-NOTE-2013-0040.pdf
IEC 61131: Programming languages for programmable logic controllers (2013)
Rausch, M., Krogh, B.: Formal verification of PLC programs. In: Proc. of the American Control Conference, pp. 234–238 (1998)
Bauer, N., Engell, S., Huuck, R., Lohmann, S., Lukoschus, B., Remelhe, M., Stursberg, O.: Verification of PLC programs given as 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. 517–540. Springer, Heidelberg (2004)
Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of PLC programs written in Instruction List. In: Proc. of Int. Conf. on Systems, Man, and Cybernetics 2000, pp. 2449–2454. Argos Press (2000)
Pavlović, O., Ehrich, H.D.: Model checking PLC software written in function block diagram. In: International Conference on Software Testing, pp. 439–448 (2010)
Soliman, D., Frey, G.: Verification and validation of safety applications based on PLCopen safety function blocks. Control Engineering Practice 19(9), 929–946 (2011)
Gourcuff, V., de Smet, O., Faure, J.M.: Improving large-sized PLC programs verification using abstractions. In: 17th IFAC World Congress (2008)
Lange, T., Neuhäußer, M., Noll, T.: Speeding up the safety verification of programmable logic controller code. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 44–60. Springer, Heidelberg (2013)
Biallas, S., Brauer, J., Kowalewski, S.: Counterexample-guided abstraction refinement for PLCs. In: Proc. of 5th International Workshop on Systems Software Verification, pp. 2–12. USENIX Association (2010)
Blanco, E., et al.: UNICOS evolution: CPC version 6. In: 12th ICALEPCS (2011)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press (1999)
Cavada, R., Cimatti, A., Jochim, C.A., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV 2.5 User Manual. FBK-irst (2011)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Cooper, K.D., Torczon, L.: Engineering a Compiler, 2nd edn. Morgan Kaufmann Publishers Inc. (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Darvas, D., Fernández Adiego, B., Vörös, A., Bartha, T., Blanco Viñuela, E., González Suárez, V.M. (2014). Formal Verification of Complex Properties on PLC Programs. In: Ábrahám, E., Palamidessi, C. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2014. Lecture Notes in Computer Science, vol 8461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43613-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-662-43613-4_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43612-7
Online ISBN: 978-3-662-43613-4
eBook Packages: Computer ScienceComputer Science (R0)