Industrial Controls
Page tree
Skip to end of metadata
Go to start of metadata

Formal methods applied to PLC programs

Purpose

Developing safe and robust PLC (Programmable Logic Controller) control systems is a common goal for control engineers. Traditionally, testing techniques have been applied for that purpose, but some obvious problems remain unsolved as typically the exhaustive testing of a non-trivial system is not possible.

The goal of this project is to provide a methodology which guaranties that a PLC program is compliant with the required specification. This methodology is based on applying automated formal verification methods to PLC programs, hiding the complexity from the control engineers whenever possible. For that purpose, the methodology is supported by a specialized tool which creates the formal models automatically and helps the user to formalize the project specifications.

Approach

The formal models are generated automatically out of the PLC programs to verify. Currently ST (Structured Text),  IL (Instruction List) and SFC (Sequential Function Chart) languages are included in the methodology, as they are widely used at CERN. In addition, the methodology is meant to be general and open to any verification tool. For that reason the methodology is based on an Intermediate Model (IM) which is the central point of the methodology, which have 5 steps:

  1. Formalization of the requirements.
  2. Transformation from PLC code to the IM.
  3. Reduction of the state space of the IM.
  4. Transformation from the IM to the input language of the verification tools (Currently nuXmv, UPPAAL and BIP and included).
  5. Verification and analysis of the results.

 


All these steps are hidden from the control engineer and the methodology is integrated in the traditional development of PLC programs as it is shown in the following figure. 

Status

First experiments on UNICOS CPC-based PLC programs have been performed and outstanding results have been already achieved. The project is still in its development phase.

We are developing a proof-of-concept tool named PLCverif.

Selected publications

  • B. Fernández Adiego, D. Darvas, E. Blanco Viñuela, J-C. Tournier, S. Bliudze, J. O. Blech, V. M. González Suárez: Applying model checking to industrial-sized PLC programs. IEEE Transactions on Industrial Informatics, Vol. 11, Issue 6, pp. 1400-1410, 2015.  [Paper on IEEExplore]  [bib]
  • D. Darvas, I. Majzik, E. Blanco Viñuela: Formal verification of safety PLC based control software. In E. Ábrahám, M. Huisman (Eds.), Integrated Formal Methods, vol. 9681 of Lecture Notes in Computer Science. Springer, 2016.  [Paper]  (The original publication is available at www.springerlink.com)
  • D. Darvas, B. Fernández Adiego, E. Blanco Viñuela: PLCverif: A tool to verify PLC programs based on model checking techniques. In Proc. of the 15th International Conference on Accelerator and Large Experimental Physics Control Systems, pp. 911-914, 2015.   [Paper]

Publications

  • B. Fernández Adiego, E. Blanco Viñuela, J-C. Tournier, V. M. González Suárez: Model-based automated testing of critical PLC programs. In Proc. of 11th IEEE International Conference on Industrial Informatics (INDIN), Bochum, Germany, 07/2013. [Paper on IEEExplore]
  • B. Fernández Adiego,  E. Blanco Viñuela, A. Merezhin: Testing and formal verification of PLC code for process control. In Proc. of the 14th International Conference on Accelerator and Large Experimental Physics Control Systems, San Francisco, CA, USA, 06/11/2013.  [Paper on CDS]
  • D. Darvas, B. Fernández Adiego, E. Blanco Viñuela: Transforming PLC programs into formal models for verification purposes. CERN Internal Note, CERN-ACC-NOTE-2013-0040, 2013. [Paper on CDS]
  • B. Fernández Adiego, D. Darvas, J-C. Tournier, E. Blanco Viñuela, V. M. González Suárez: Bringing automated model checking to PLC program development – A CERN case study. In J-J. Lesage et al. (Eds.): Preprints of the 12th International Workshop on Discrete Event Systems (WODES 2014), pp. 394-399, Paris, France, 05/2014. [Paper on CDS]  [bib]
  • D. Darvas, B. Fernández Adiego, A. Vörös, T. Bartha, E. Blanco Viñuela, V. M. González Suárez: Formal verification of complex properties on PLC programs. In E. Ábráham and C. Palamidessi (Eds.): Formal Techniques for Distributed Objects, Components, and Systems, vol. 8461 of Lecture Notes in Computer Science, pp. 284-299, Springer, 2014.   [Paper on CDS]  [bib] (The original publication is available at  www.springerlink.com)
  • D. Darvas, B. Fernández Adiego, J-C. Tournier, E. Blanco Viñuela, J. O. Blech, V. M. González Suárez: Automated generation of formal models from ST control programs for verification purposes. CERN Internal Note, CERN-ACC-NOTE-2014-0037, 2014. [Paper on CDS]
  • B. Fernández Adiego, D. Darvas, E. Blanco Viñuela, J-C. Tournier, V. M. González Suárez, J. O. Blech: Modelling and formal verification of timing aspects in large PLC programs. In: Proc. of IFAC World Congress 2014, Cape Town, South Africa, 08/2014.  [Paper on CDS] [bib]
  • B. Fernández Adiego: Bringing automated formal verification to PLC program development. PhD Thesis, University of Oviedo, 2014.  [Thesis on CDS]
  • D. Darvas, I. Majzik, E. Blanco Viñuela: Generic representation of PLC programming languages for formal verification. In Proc. of the 23rd PhD Mini-Symposium of the Department of Measurement and Information Systems, Budapest University of Technology and Economics, 2016. DOI:  10.5281/zenodo.51064 
  • D. Darvas, I. Majzik, E. Blanco Viñuela: PLC program translation for verification purposes. Periodica Polytechnica, Electrical Engineering and Computer Science, Vol. 61, Issue 2, pp. 151-165, 2017. DOI: 10.3311/PPee.9743
  • G. Sallai, D. Darvas, E. Blanco Viñuela. Translation of PLC programs to x86 for simulation and verification. CERN Summer student report CERN-STUDENTS-Note-2017-186, CERN, 2017. [Paper on CDS]
  • G. Sallai, D. Darvas, E. Blanco Viñuela. Testing, simulation, and visualisation of PLC programs using x86 code generation. Techical report, EDMS 1844850, CERN, 2017. [Paper on EDMS]
  • D. Darvas, E. Blanco Viñuela, I. Majzik. What is special about PLC software model checking? In Proc. of the 16th International Conference on Accelerator and Large Experimental Physics Control Systems, 2017. [Paper] [Poster]
  • B. Fernández Adiego, D. Darvas, E. Blanco Viñuela, G. Sallai, I. Prieto Diaz, G. Lee, B. Avinashkrishna, Y. C. Gaikwad, S. Sreekuttan, R. Pedica. Appyling model checking to critical PLC applications: An ITER case study. In Proc. of the 16th International Conference on Accelerator and Large Experimental Physics Control Systems, 2017. [Paper] [Poster]
  • I. D. Lopez-Miguel, B. Fernández Adiego, J.-C. Tournier, E. Blanco Viñuela, J. A. Rodriguez-Aguilar. Simplification of numeric variables for PLC model checking. In Proc. of the MEMOCODE '21: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design. [Paper]
  • B. Fernández Adiego, I. D. Lopez-Miguel, J-C. Tournier, E. Blanco Viñuela, T. Ladzinski, F. Havart. Applying model checking to highly-configurable safety critical software: the SPS-PPS PLC program. In Proc. of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems, 2021. [Paper]
  • I. D. Lopez-Miguel, J-C. Tournier, B. Fernandez. PLCverif: status of a formal verification tool for Programmable Logic Controller. In Proc. of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems, 2021. [Paper]

Related Presentations

  • B. Fernández Adiego: Formal verification in Industrial Control Systems. Presented at the ICE Tea, 14 February 2014. [Slides]
  • D. Darvas: Domain-specific languages – What, how and when? Presented at the ICE Tea, 21 February 2014. [Slides]
  • B. Fernández Adiego: Formal methods applied to PLC code verification. Presented at the Advanced Control Engineering: Academia - Industry workshop, 2-3 June 2014. [Slides on Indico]   

  • B. Fernández Adiego: Bringing Automated Formal Verification to PLC Program Development. Presented on the PhD Thesis defense, 19 December 2014.  [Slides]

  • D. Darvas: Formal verification of industrial control systems... at CERN. Presented at the 1st Developers@CERN Forum on Software Quality, Reliability and Testing, 28-29 September 2015. [Slides on Indico]

  • B. Fernández Adiego: Automated Formal Verification of PLC Programs. Presented at the CERN-ESTEREL Technical Seminar , 21 January 2016.  [Slides on Indico]     
  • D. Darvas: Formal verification of industrial control systems. Presented at the 3th Workshop on PLC/COTS-based Interlock and Protection Systems, 01-02 February 2016.  [Slides on Indico]
  • D. Darvas: Practice-oriented formal methods to support the software development of industrial control systems. Presented on the PhD Thesis defense, 15 May 2017. [Slides]
  • Gy. Sallai: Exploring the possible uses of translating PLC code to C (and more). Presented at CERN, 29 August 2017. [Slides]
  • D. Darvas: Finding bugs in the LHC: Verification methods for PLC programs. Presented at the Alpine Verification Meeting 2017, 18 September 2017. [Slides]
  • B. Fernandez: Formal methods to verify PLC code and its applicability to safety systems. CERN BE seminars [Slides]

Contact persons