Research Article
BibTex RIS Cite

Year 2023, Volume: 7 Issue: 1, 13 - 28, 21.06.2023

Özgür Turay Kaymakçı Muhammed Ali Nur Öz

https://doi.org/10.38088/jise.1120186

Abstract

References

  • [1] Zhou, M.; Wan, H.; Wang, R.; Song, X.; Su, C.; Gu, M.; Sun, J. (2013). Formal component-based modeling and synthesis for PLC systems, Computers in Industry, Vol. 64, No. 8, 1022–1034. doi:10.1016/j.compind.2013.07.003
  • [2] Ljungkrantz, O.; Akesson, K.; Yuan, C.; Fabian, M. (2012). Towards Industrial Formal Specification of Programmable Safety Systems, IEEE Transactions on Control Systems Technology, Vol. 20, No. 6, 1567–1574Presented at the IEEE Transactions on Control Systems Technology. doi:10.1109/TCST.2011.2169262
  • [3] Vieira, A. D.; Santos, E. A. P.; de Queiroz, M. H.; Leal, A. B.; de Paula Neto, A. D.; Cury, J. E. R. (2017). A Method for PLC Implementation of Supervisory Control of Discrete Event Systems, IEEE Transactions on Control Systems Technology, Vol. 25, No. 1, 175–191Presented at the IEEE Transactions on Control Systems Technology. doi:10.1109/TCST.2016.2544702
  • [4] Chen, C.; Hu, H. (2015). Maximally permissive distributed control of automated manufacturing systems with assembly operations using Petri nets, 2015 IEEE International Conference on Automation Science and Engineering (CASE)Presented at the 2015 IEEE International Conference on Automation Science and Engineering (CASE), , 532–538. doi:10.1109/CoASE.2015.7294134
  • [5] List, G. F.; Mashayekhi, M. (2016). A Modular Colored Stochastic Petri Net for Modeling and Analysis of Signalized Intersections, IEEE Transactions on Intelligent Transportation Systems, Vol. 17, No. 3, 701–713Presented at the IEEE Transactions on Intelligent Transportation Systems. doi:10.1109/TITS.2015.2483324
  • [6] Wang, X.; Mahulea, C.; Silva, M. (2013). Fault Diagnosis Graph of time Petri nets, 2013 European Control Conference (ECC)Presented at the 2013 European Control Conference (ECC), , 2459–2464. doi:10.23919/ECC.2013.6669417
  • [7] Rösch, S.; Ulewicz, S.; Provost, J.; Vogel-Heuser, B. (2015). Review of Model-Based Testing Approaches in Production Automation and Adjacent Domains—Current Challenges and Research Gaps, Journal of Software Engineering and Applications, Vol. 08, No. 09, 499–519. doi:10.4236/jsea.2015.89048
  • [8] Ovatman, T.; Aral, A.; Polat, D.; Ünver, A. O. (2016). An overview of model checking practices on verification of PLC software, Software & Systems Modeling, Vol. 15, No. 4, 937–960. doi:10.1007/s10270-014-0448-7
  • [9] Bauer, N.; Engell, S.; Huuck, R.; Lohmann, S.; Lukoschus, B.; Remelhe, M.; Stursberg, O. (2004). Verification of PLC Programs Given as Sequential Function Charts, H. Ehrig; W. Damm; J. Desel; M. Große-Rhode; W. Reif; E. Schnieder; E. Westkämper (Eds.), Integration of Software Specification Techniques for Applications in Engineering: Priority Program SoftSpez of the German Research Foundation (DFG), Final Report, Springer, Berlin, Heidelberg, 517–540. doi:10.1007/978-3-540-27863-4_28
  • [10] Mertke, T.; Frey, G. (2001). Formal verification of PLC programs generated from signal interpreted Petri nets, 2001 IEEE International Conference on Systems, Man and Cybernetics. e-Systems and e-Man for Cybernetics in Cyberspace (Cat.No.01CH37236) (Vol. 4)Presented at the 2001 IEEE International Conference on Systems, Man and Cybernetics. e-Systems and e-Man for Cybernetics in Cyberspace (Cat.No.01CH37236), , 2700–2705 vol.4. doi:10.1109/ICSMC.2001.972974
  • [11] Alenljung, T.; Lennartson, B.; Hosseini, M. N. (2012). Sensor Graphs for Discrete Event Modeling Applied to Formal Verification of PLCs, IEEE Transactions on Control Systems Technology, Vol. 20, No. 6, 1506–1521Presented at the IEEE Transactions on Control Systems Technology. doi:10.1109/TCST.2011.2168607
  • [12] Nellen, J.; Driessen, K.; Neuhäußer, M.; Ábrahám, E.; Wolters, B. (2016). Two CEGAR-based approaches for the safety verification of PLC-controlled plants, Information Systems Frontiers, Vol. 18, No. 5, 927–952. doi:10.1007/s10796-016-9671-9
  • [13] Carlsson, H.; Svensson, B.; Danielsson, F.; Lennartson, B. (2012). Methods for Reliable Simulation-Based PLC Code Verification, IEEE Transactions on Industrial Informatics, Vol. 8, No. 2, 267–278Presented at the IEEE Transactions on Industrial Informatics. doi:10.1109/TII.2011.2182653
  • [14] Rankin, D. J.; Jiang, J. (2011). A Hardware-in-the-Loop Simulation Platform for the Verification and Validation of Safety Control Systems, IEEE Transactions on Nuclear Science, Vol. 58, No. 2, 468–478Presented at the IEEE Transactions on Nuclear Science. doi:10.1109/TNS.2010.2103325
  • [15] Park, S. C.; Park, C. M.; Wang, G.-N.; Kwak, J.; Yeo, S. (2008). PLCStudio: Simulation based PLC code verification, 2008 Winter Simulation ConferencePresented at the 2008 Winter Simulation Conference, , 222–228. doi:10.1109/WSC.2008.4736071
  • [16] Patil, M. M.; Subbaraman, S.; Joshi, S. (2011). Exploring Integrated Circuit Verification Methodology for Verification and Validation of PLC Systems, 2011 International Symposium on Electronic System DesignPresented at the 2011 International Symposium on Electronic System Design, , 88–93. doi:10.1109/ISED.2011.47
  • [17] Koo, L.-J.; Park, C. M.; Lee, C. H.; Park, S.; Wang, G.-N. (2011). Simulation framework for the verification of PLC programs in automobile industries, International Journal of Production Research, Vol. 49, No. 16, 4925–4943. doi:10.1080/00207543.2010.492404
  • [18] Wang, R.; Guan, Y.; Luo, L.; Song, X.; Zhang, J. (2013). Formal Modelling of PLC Systems by BIP Components, 2013 IEEE 37th Annual Computer Software and Applications ConferencePresented at the 2013 IEEE 37th Annual Computer Software and Applications Conference, , 512–518. doi:10.1109/COMPSAC.2013.85
  • [19] Zhang, M.; Chen, C.-Y.; Kao, B.-C.; Qamsane, Y.; Shao, Y.; Lin, Y.; Shi, E.; Mohan, S.; Barton, K.; Moyne, J.; Mao, Z. M. (2019). Towards Automated Safety Vetting of PLC Code in Real-World Plants, 2019 IEEE Symposium on Security and Privacy (SP)Presented at the 2019 IEEE Symposium on Security and Privacy (SP), , 522–538. doi:10.1109/SP.2019.00034
  • [20] Fernández Adiego, B.; Darvas, D.; Viñuela, E. B.; Tournier, J.-C.; Bliudze, S.; Blech, J. O.; González Suárez, V. M. (2015). Applying Model Checking to Industrial-Sized PLC Programs, IEEE Transactions on Industrial Informatics, Vol. 11, No. 6, 1400–1410Presented at the IEEE Transactions on Industrial Informatics. doi:10.1109/TII.2015.2489184
  • [21] Xiao, L.; Li, M.; Gu, M.; Sun, J. (2014). A hierarchy framework on compositional verification for PLC software, 2014 IEEE 5th International Conference on Software Engineering and Service SciencePresented at the 2014 IEEE 5th International Conference on Software Engineering and Service Science, , 204–207. doi:10.1109/ICSESS.2014.6933545
  • [22] Ulewicz, S.; Vogel-Heuser, B.; Ulbrich, M.; Weigl, A.; Beckert, B. (2015). Proving equivalence between control software variants for Programmable Logic Controllers, 2015 IEEE 20th Conference on Emerging Technologies Factory Automation (ETFA)Presented at the 2015 IEEE 20th Conference on Emerging Technologies Factory Automation (ETFA), , 1–5. doi:10.1109/ETFA.2015.7301603
  • [23] He, N.; Oke, V.; Allen, G. (2016). Model-based verification of PLC programs using Simulink design, 2016 IEEE International Conference on Electro Information Technology (EIT)Presented at the 2016 IEEE International Conference on Electro Information Technology (EIT), , 0211–0216. doi:10.1109/EIT.2016.7535242
  • [24] Adiego, B. F.; Lopez-Miguel, I. D.; Tournier, J.-C.; Blanco, E.; Ladzinski, T.; Havart, F. (2022). Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program, Proceedings of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems, Vol. ICALEPCS2021, 5 pages, 0.178 MB. doi:10.18429/JACoW-ICALEPCS2021-WEPV042
  • [25] Ljungkrantz, O.; Akesson, K.; Fabian, M.; Yuan, C. (2010). Formal Specification and Verification of Industrial Control Logic Components, IEEE Transactions on Automation Science and Engineering, Vol. 7, No. 3, 538–548Presented at the IEEE Transactions on Automation Science and Engineering. doi:10.1109/TASE.2009.2031095
  • [26] Bel Mokadem, H.; Bérard, B.; Gourcuff, V.; De Smet, O.; Roussel, J.-M. (2010). Verification of a Timed Multitask System With Uppaal, IEEE Transactions on Automation Science and Engineering, Vol. 7, No. 4, 921–932Presented at the IEEE Transactions on Automation Science and Engineering. doi:10.1109/TASE.2010.2050199

A New Method for Verification and Evaluation of PLC Software

Year 2023, Volume: 7 Issue: 1, 13 - 28, 21.06.2023

Özgür Turay Kaymakçı Muhammed Ali Nur Öz

https://doi.org/10.38088/jise.1120186

Abstract

Varying market demands and changes in production standards require production systems to be effortlessly modifiable and quickly operational. On the other hand, designing, developing, and testing the control system of a new production system prove costly and time-consuming. Therefore, most engineers write code intuitively and apply basic and insufficient tests. Moreover, most of the code developed for industrial control systems is still written manually using the ladder programming language. At the same time, almost all code development platforms support users with only manual test interfaces. This causes the testing process to be very long and laborious. In addition, not all possible input and output combinations of the code can be tested most of the time. This is a serious handicap, especially for safety-related systems. This study aims to develop a reusable and quickly implementable method that will accurately translate RTC program and the behavior of RTC in a modular Petri net model. Through this translated model, the system and safety requirements written in the Computation Tree Logic can be verified. An advantage of this method is that it does not require a plant model which makes it reusable for new plants and provides a quick verification method for code written intuitively. A case study is given to demonstrate the correctness of our method.

Keywords

Industrial Automation Programmable Logic Controller (PLC) Code Verification Safety

References

  • [1] Zhou, M.; Wan, H.; Wang, R.; Song, X.; Su, C.; Gu, M.; Sun, J. (2013). Formal component-based modeling and synthesis for PLC systems, Computers in Industry, Vol. 64, No. 8, 1022–1034. doi:10.1016/j.compind.2013.07.003
  • [2] Ljungkrantz, O.; Akesson, K.; Yuan, C.; Fabian, M. (2012). Towards Industrial Formal Specification of Programmable Safety Systems, IEEE Transactions on Control Systems Technology, Vol. 20, No. 6, 1567–1574Presented at the IEEE Transactions on Control Systems Technology. doi:10.1109/TCST.2011.2169262
  • [3] Vieira, A. D.; Santos, E. A. P.; de Queiroz, M. H.; Leal, A. B.; de Paula Neto, A. D.; Cury, J. E. R. (2017). A Method for PLC Implementation of Supervisory Control of Discrete Event Systems, IEEE Transactions on Control Systems Technology, Vol. 25, No. 1, 175–191Presented at the IEEE Transactions on Control Systems Technology. doi:10.1109/TCST.2016.2544702
  • [4] Chen, C.; Hu, H. (2015). Maximally permissive distributed control of automated manufacturing systems with assembly operations using Petri nets, 2015 IEEE International Conference on Automation Science and Engineering (CASE)Presented at the 2015 IEEE International Conference on Automation Science and Engineering (CASE), , 532–538. doi:10.1109/CoASE.2015.7294134
  • [5] List, G. F.; Mashayekhi, M. (2016). A Modular Colored Stochastic Petri Net for Modeling and Analysis of Signalized Intersections, IEEE Transactions on Intelligent Transportation Systems, Vol. 17, No. 3, 701–713Presented at the IEEE Transactions on Intelligent Transportation Systems. doi:10.1109/TITS.2015.2483324
  • [6] Wang, X.; Mahulea, C.; Silva, M. (2013). Fault Diagnosis Graph of time Petri nets, 2013 European Control Conference (ECC)Presented at the 2013 European Control Conference (ECC), , 2459–2464. doi:10.23919/ECC.2013.6669417
  • [7] Rösch, S.; Ulewicz, S.; Provost, J.; Vogel-Heuser, B. (2015). Review of Model-Based Testing Approaches in Production Automation and Adjacent Domains—Current Challenges and Research Gaps, Journal of Software Engineering and Applications, Vol. 08, No. 09, 499–519. doi:10.4236/jsea.2015.89048
  • [8] Ovatman, T.; Aral, A.; Polat, D.; Ünver, A. O. (2016). An overview of model checking practices on verification of PLC software, Software & Systems Modeling, Vol. 15, No. 4, 937–960. doi:10.1007/s10270-014-0448-7
  • [9] Bauer, N.; Engell, S.; Huuck, R.; Lohmann, S.; Lukoschus, B.; Remelhe, M.; Stursberg, O. (2004). Verification of PLC Programs Given as Sequential Function Charts, H. Ehrig; W. Damm; J. Desel; M. Große-Rhode; W. Reif; E. Schnieder; E. Westkämper (Eds.), Integration of Software Specification Techniques for Applications in Engineering: Priority Program SoftSpez of the German Research Foundation (DFG), Final Report, Springer, Berlin, Heidelberg, 517–540. doi:10.1007/978-3-540-27863-4_28
  • [10] Mertke, T.; Frey, G. (2001). Formal verification of PLC programs generated from signal interpreted Petri nets, 2001 IEEE International Conference on Systems, Man and Cybernetics. e-Systems and e-Man for Cybernetics in Cyberspace (Cat.No.01CH37236) (Vol. 4)Presented at the 2001 IEEE International Conference on Systems, Man and Cybernetics. e-Systems and e-Man for Cybernetics in Cyberspace (Cat.No.01CH37236), , 2700–2705 vol.4. doi:10.1109/ICSMC.2001.972974
  • [11] Alenljung, T.; Lennartson, B.; Hosseini, M. N. (2012). Sensor Graphs for Discrete Event Modeling Applied to Formal Verification of PLCs, IEEE Transactions on Control Systems Technology, Vol. 20, No. 6, 1506–1521Presented at the IEEE Transactions on Control Systems Technology. doi:10.1109/TCST.2011.2168607
  • [12] Nellen, J.; Driessen, K.; Neuhäußer, M.; Ábrahám, E.; Wolters, B. (2016). Two CEGAR-based approaches for the safety verification of PLC-controlled plants, Information Systems Frontiers, Vol. 18, No. 5, 927–952. doi:10.1007/s10796-016-9671-9
  • [13] Carlsson, H.; Svensson, B.; Danielsson, F.; Lennartson, B. (2012). Methods for Reliable Simulation-Based PLC Code Verification, IEEE Transactions on Industrial Informatics, Vol. 8, No. 2, 267–278Presented at the IEEE Transactions on Industrial Informatics. doi:10.1109/TII.2011.2182653
  • [14] Rankin, D. J.; Jiang, J. (2011). A Hardware-in-the-Loop Simulation Platform for the Verification and Validation of Safety Control Systems, IEEE Transactions on Nuclear Science, Vol. 58, No. 2, 468–478Presented at the IEEE Transactions on Nuclear Science. doi:10.1109/TNS.2010.2103325
  • [15] Park, S. C.; Park, C. M.; Wang, G.-N.; Kwak, J.; Yeo, S. (2008). PLCStudio: Simulation based PLC code verification, 2008 Winter Simulation ConferencePresented at the 2008 Winter Simulation Conference, , 222–228. doi:10.1109/WSC.2008.4736071
  • [16] Patil, M. M.; Subbaraman, S.; Joshi, S. (2011). Exploring Integrated Circuit Verification Methodology for Verification and Validation of PLC Systems, 2011 International Symposium on Electronic System DesignPresented at the 2011 International Symposium on Electronic System Design, , 88–93. doi:10.1109/ISED.2011.47
  • [17] Koo, L.-J.; Park, C. M.; Lee, C. H.; Park, S.; Wang, G.-N. (2011). Simulation framework for the verification of PLC programs in automobile industries, International Journal of Production Research, Vol. 49, No. 16, 4925–4943. doi:10.1080/00207543.2010.492404
  • [18] Wang, R.; Guan, Y.; Luo, L.; Song, X.; Zhang, J. (2013). Formal Modelling of PLC Systems by BIP Components, 2013 IEEE 37th Annual Computer Software and Applications ConferencePresented at the 2013 IEEE 37th Annual Computer Software and Applications Conference, , 512–518. doi:10.1109/COMPSAC.2013.85
  • [19] Zhang, M.; Chen, C.-Y.; Kao, B.-C.; Qamsane, Y.; Shao, Y.; Lin, Y.; Shi, E.; Mohan, S.; Barton, K.; Moyne, J.; Mao, Z. M. (2019). Towards Automated Safety Vetting of PLC Code in Real-World Plants, 2019 IEEE Symposium on Security and Privacy (SP)Presented at the 2019 IEEE Symposium on Security and Privacy (SP), , 522–538. doi:10.1109/SP.2019.00034
  • [20] Fernández Adiego, B.; Darvas, D.; Viñuela, E. B.; Tournier, J.-C.; Bliudze, S.; Blech, J. O.; González Suárez, V. M. (2015). Applying Model Checking to Industrial-Sized PLC Programs, IEEE Transactions on Industrial Informatics, Vol. 11, No. 6, 1400–1410Presented at the IEEE Transactions on Industrial Informatics. doi:10.1109/TII.2015.2489184
  • [21] Xiao, L.; Li, M.; Gu, M.; Sun, J. (2014). A hierarchy framework on compositional verification for PLC software, 2014 IEEE 5th International Conference on Software Engineering and Service SciencePresented at the 2014 IEEE 5th International Conference on Software Engineering and Service Science, , 204–207. doi:10.1109/ICSESS.2014.6933545
  • [22] Ulewicz, S.; Vogel-Heuser, B.; Ulbrich, M.; Weigl, A.; Beckert, B. (2015). Proving equivalence between control software variants for Programmable Logic Controllers, 2015 IEEE 20th Conference on Emerging Technologies Factory Automation (ETFA)Presented at the 2015 IEEE 20th Conference on Emerging Technologies Factory Automation (ETFA), , 1–5. doi:10.1109/ETFA.2015.7301603
  • [23] He, N.; Oke, V.; Allen, G. (2016). Model-based verification of PLC programs using Simulink design, 2016 IEEE International Conference on Electro Information Technology (EIT)Presented at the 2016 IEEE International Conference on Electro Information Technology (EIT), , 0211–0216. doi:10.1109/EIT.2016.7535242
  • [24] Adiego, B. F.; Lopez-Miguel, I. D.; Tournier, J.-C.; Blanco, E.; Ladzinski, T.; Havart, F. (2022). Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program, Proceedings of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems, Vol. ICALEPCS2021, 5 pages, 0.178 MB. doi:10.18429/JACoW-ICALEPCS2021-WEPV042
  • [25] Ljungkrantz, O.; Akesson, K.; Fabian, M.; Yuan, C. (2010). Formal Specification and Verification of Industrial Control Logic Components, IEEE Transactions on Automation Science and Engineering, Vol. 7, No. 3, 538–548Presented at the IEEE Transactions on Automation Science and Engineering. doi:10.1109/TASE.2009.2031095
  • [26] Bel Mokadem, H.; Bérard, B.; Gourcuff, V.; De Smet, O.; Roussel, J.-M. (2010). Verification of a Timed Multitask System With Uppaal, IEEE Transactions on Automation Science and Engineering, Vol. 7, No. 4, 921–932Presented at the IEEE Transactions on Automation Science and Engineering. doi:10.1109/TASE.2010.2050199
There are 26 citations in total.

Details

Primary Language English
Subjects Engineering
Journal Section Research Articles
Authors

Özgür Turay Kaymakçı 0000-0001-7553-6887

Muhammed Ali Nur Öz 0000-0002-4347-3583

Early Pub Date June 21, 2023
Publication Date June 21, 2023
Published in Issue Year 2023Volume: 7 Issue: 1

Cite

APA Kaymakçı, Ö. T., & Öz, M. A. N. (2023). A New Method for Verification and Evaluation of PLC Software. Journal of Innovative Science and Engineering, 7(1), 13-28. https://doi.org/10.38088/jise.1120186
AMA Kaymakçı ÖT, Öz MAN. A New Method for Verification and Evaluation of PLC Software. JISE. June 2023;7(1):13-28. doi:10.38088/jise.1120186
Chicago Kaymakçı, Özgür Turay, and Muhammed Ali Nur Öz. “A New Method for Verification and Evaluation of PLC Software”. Journal of Innovative Science and Engineering 7, no. 1 (June 2023): 13-28. https://doi.org/10.38088/jise.1120186.
EndNote Kaymakçı ÖT, Öz MAN (June 1, 2023) A New Method for Verification and Evaluation of PLC Software. Journal of Innovative Science and Engineering 7 1 13–28.
IEEE Ö. T. Kaymakçı and M. A. N. Öz, “A New Method for Verification and Evaluation of PLC Software”, JISE, vol. 7, no. 1, pp. 13–28, 2023, doi: 10.38088/jise.1120186.
ISNAD Kaymakçı, Özgür Turay - Öz, Muhammed Ali Nur. “A New Method for Verification and Evaluation of PLC Software”. Journal of Innovative Science and Engineering 7/1 (June 2023), 13-28. https://doi.org/10.38088/jise.1120186.
JAMA Kaymakçı ÖT, Öz MAN. A New Method for Verification and Evaluation of PLC Software. JISE. 2023;7:13–28.
MLA Kaymakçı, Özgür Turay and Muhammed Ali Nur Öz. “A New Method for Verification and Evaluation of PLC Software”. Journal of Innovative Science and Engineering, vol. 7, no. 1, 2023, pp. 13-28, doi:10.38088/jise.1120186.
Vancouver Kaymakçı ÖT, Öz MAN. A New Method for Verification and Evaluation of PLC Software. JISE. 2023;7(1):13-28.
 Download Cover Image


Creative Commons License

The works published in Journal of Innovative Science and Engineering (JISE) are licensed under a  Creative Commons Attribution-NonCommercial 4.0 International License.