Page History

...

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. 

...

• 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 In Proc. of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems, 2021. In press. [Paper]
• I. D. Lopez-Miguel, J-C. Tournier, B. Fernandez. PLCverif: status of a formal verification tool for Programmable Logic Controller.  In In Proc. of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems, 2021. In press. [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]

...