LTL-specification for development and verification of logical control programs in feedback systems

M. V. Neyzov ; E. V. Kuzmin

Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 3, pp. 240-279.

Résumé

The article continues the series of publications on the development and verification of control programs based on LTL-specifications of a special type. Earlier, a declarative LTL-specification was proposed to describe the strictly deterministic behavior of programs, ways of its verification and translation were worked out: for verification, the model checking tool nuXmv is used, and the translation is carried out into an imperative programming language ST for programmable logic controllers. When verifying the declarative LTL-specification of the behavior of programs, there may be a need to simulate the behavior of its environment. In general, it is required to ensure the possibility of constructing closed-loop systems “program-environment”. In this work, an LTL-specification of constraintly nondeterministic behavior of a Boolean variable is proposed to describe the behavior of the environment of logical control programs. This specification allows defining the behavior of Boolean feedback signals, as well as fairness conditions to exclude unrealistic scenarios of behavior. The article proposes an approach to the development and verification of logical control programs, within which the behavior model of the program environment is described in the form of constraints on the behavior of its input signals, what allows avoiding a separate detailed representation of the processes of the environment operation. As a result, the obtained behavior model of the closed-loop system “program-environment” provides a number of advantages: simplification of the modeling process, reduction of the state space of the verified model, and reduction of verification time. If it is impossible to reduce the behavior of the environment to the behavior of existing input signals, this approach suggests using “imaginary” sensors — additional Boolean variables that are used as an auxiliary means for describing the behavior of input signals. The purpose of introducing imaginary sensors is to compensate for missing sensors to track the specific behavior of some elements of the environment that needs to be taken into account when defining realistic behavior of the inputs of a logical control program. The proposed approach to the development and verification of programs taking into account the behavior of the environment (a control object) is demonstrated by the example of an industrial plastic molding plant.

Détail

Keywords: control software, PLC program, declarative LTL-specification, LTL-specification of constraintly nondeterministic behavior, fairness conditions, closed-loop systems verification, plant behavior model, imaginary sensor, temporal properties, model checking, nuXmv verifier, SMV-specification.

Bibliographie

[1] S. Oks and et al, “Cyber-Physical Systems in the Context of Industry 4.0: A Review, Categorization and Outlook”, Information Systems Frontiers, 2022, 1–42 | DOI | Zbl

[2] K. Zhang, Y. Shi, S. Karnouskos, T. Sauter, H. Fang, A. W. Colombo, “Advancements in Industrial Cyber-Physical Systems: An Overview and Perspectives”, IEEE Transactions on Industrial Informatics, 19:1 (2023), 716–729 | DOI

[3] S. J. Oks, Industrial Cyber-Physical Systems: Advancing Industry 4.0 from Vision to Application (MAU), 1st ed, Springer, 2024 | DOI

[4] C. Dey, S. K. Sen, Industrial Automation Technologies, 1st ed, CRC Press, 2020 | DOI

[5] K. Thramboulidis, “A CyberPhysical System-Based Approach for Industrial Automation Systems”, Computers in Industry, 72 (2015), 92–102 | DOI

[6] IEC 61131-1:2003 Programmable controllers – Part 1: General information https://webstore.iec.ch/publication/4550

[7] R. Langmann, L. F. Rojas-Pena, “A PLC as an Industry 4.0 Component”, Remote Engineering and Virtual Instrumentation, 2016, 10-–15 | DOI

[8] D. Harel, A. Pnueli, “On the Development of Reactive Systems”, Logics and Models of Concurrent Systems, 13 (1985), 477–498 | DOI | MR | Zbl

[9] A. Maurya, D. Kumar, “Reliability of safety-critical systems: A state-of-the-art review”, Quality and Reliability Engineering International, 36, Aug (2020) | DOI | MR

[10] D. J. Smith, K. G. Simpson, The Safety Critical Systems Handbook, 5th, Butterworth-Heinemann, 2020

[11] V. Vyatkin, “Software Engineering in Industrial Automation: State-of-the-Art Review”, IEEE Transactions on Industrial Informatics, 9:3 (2013), 1234–1249 | DOI

[12] S. Mitra, “Verifying Cyber-Physical Systems: A Path to Safe Autonomy”, Cyber Physical Systems Series, MIT Press, 2021 | MR

[13] V. DTSilva, D. Kroening, G. Weissenbacher, “A Survey of Automated Techniques for Formal Software Verification”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27 (2008), 1165–1178 | DOI

[14] R. Sinha, S. Patil, L. Gomes, V. Vyatkin, “A Survey of Static Formal Methods for Building Dependable Industrial Automation Systems”, IEEE Transactions on Industrial Informatics, 15:7 (2019), 3772–3783 | DOI

[15] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking, 1st, Springer, 2018 | DOI | MR | Zbl

[16] Y. G. Karpov, MODEL CHECKING. Verification of Parallel and Distributed Program Systems, BHV-Peterburg, 2010, 560 pp. (in Russian)

[17] E. M. Clarke, O. Grumberg, D. Peled, Verification of Program Models: Model Checking, Transl. from English to Russian, MCNMO, 2002, 416 pp.

[18] A. Pnueli, “Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends”, Current Trends in Concurrency, Lecture Notes in Computer Science, 224, Springer, 1986, 510–584 | DOI | MR

[19] K. Schneider, J. Shabolt, J. G. Taylor, Verification of reactive systems: formal methods and algorithms (EATCS), 1st ed, Springer, 2004 | DOI | MR

[20] Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems: Safety, 1st ed, Springer, 2012 | DOI

[21] J. Galvao, C. Oliveira, and et al, “Formal Verification: Focused on the Verification Using a Plant Model”, Innovation, Engineering and Entrepreneurship, Springer, 2019, 124–131 | DOI

[22] G. Frey, L. Litz, “Formal Methods in PLC Programming”, IEEE International Conference On Systems, Man and Cybernetics, v. 4, 2000, 2431–2436 | DOI

[23] J. M. Machado, B. Denis, and et al, “Logic Controllers Dependability Verification Using a Plant Model”, IFAC Proceedings Volumes, 39:17 (2006), 37–42 | DOI

[24] A. A. Shalyto, “Logic Control and YReactive Systems: Algorithmization and Programming”, Automation and Remote Control, 62:1 (2001), 1–29 | DOI | MR | Zbl

[25] E. Kuzmin, D. Ryabukhin, V. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors”, Modeling and Analysis of Information Systems, 21:4 (2014), 75–90 (in Russian) | DOI | MR

[26] E. Kuzmin, D. Ryabukhin, V. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors”, Automatic Control and Computer Sciences, 48:7 (2014), 602–614 | DOI

[27] M. Neyzov, E. Kuzmin, “LTL-specification for Development and Verification of Control Programs”, Modeling and Analysis of Information Systems, 30:4 (2023), 308–339 (in Russian) | DOI

[28] M. Neyzov, E. Kuzmin, “Verification of Declarative LTL-specification of Control Programs Behavior”, Modeling and Analysis of Information Systems, 31:2 (2024), 120–141 (in Russian) | DOI | MR

[29] nuXmv home, https://nuxmv.fbk.eu/

[30] M. Frappier, B. Fraikin, R. Chossart, R. Chane-Yack-Fa, M. Ouenzar, “Comparison of Model Checking Tools for Information Systems”, Formal Methods and Software Engineering, LNCS, 6447, Springer, 2010, 581–596 | DOI

[31] Spot home, https://spot.lre.epita.fr/

[32] M. Xavier, S. Patil, V. Dubinin, V. Vyatkin, “Formal Modelling, Analysis, and Synthesis of Modular Industrial Systems Inspired by Net Condition/Event Systems”, Applications and Theory of Petri Nets and Concurrency, 2023, 16–33 | DOI | MR

[33] V. Vyatkin, H. M. Hanisch, C. Pang, C. H. Yang, “Closed-Loop Modeling in Future Automation System Engineering and Validation”, IEEE Transactions on Systems, Man, and Cybernetics, Part C (Applications and Reviews), 39:1 (2009), 17–28 | DOI

[34] A. Lobov, J. Lastra, R. Tuokko, “Application of UML in Plant Modeling for Model-Based Verification: UML Translation to TNCES”, IEEE Industrial Informatics, 2005, 495–501 | DOI

[35] A. Lobov, J. Lastra, R. Tuokko, “On Controller and Plant Modeling for Model-Based Formal Verification”, IEEE Emerging Technologies and Factory Automation, v. 1, 2005, 121–128 | DOI

[36] S. Preuße, Technologies for Engineering Manufacturing Systems Control in Closed Loop, 10th ed, Logos Verlag Berlin GmbH, 2013

[37] S. Patil, S. Bhadra, V. Vyatkin, “Closed-Loop Formal Verification Framework with Non-Determinism”, Configurable by Meta-Modelling, IEEE Industrial Electronics Society, 2011, 3770–3775 | DOI

[38] S. Patil, V. Vyatkin, M. Sorouri, “Formal Verification of Intelligent Mechatronic Systems with Decentralized Control Logic”, IEEE Emerging Technologies Factory Automation, 2012, 1–7 | DOI

[39] S. Patil, V. Vyatkin, C. Pang, “Counterexample-Guided Simulation Framework for Formal Verification of Flexible Automation Systems”, IEEE Industrial Informatics, 2015, 1192–1197 | DOI

[40] C. Gerber, S. Preuße, H. M. Hanisch, “A Complete Framework for Controller Verification in Manufacturing”, IEEE Emerging Technologies Factory Automation, 2010, 1–9 | DOI

[41] S. Preu?e, H. C. Lapp, H. M. Hanisch, “Closed-Loop System Modeling, Validation, and Verification”, IEEE Emerging Technologies Factory Automation, 2012, 1–8 | DOI

[42] J. Machado, B. Denis, J. J. Lesage, “A Generic Approach to Build Plant Models for DES Verification Purposes”, International Workshop on Discrete Event Systems, 2006, 407–412 | DOI

[43] J. Machado, E. Seabra, and et al, “Safe Controllers Design for Industrial Automation Systems”, Computers Industrial Engineering, 60:4 (2011), 635–653 | DOI

[44] M. Perin, J. M. Faure, “Building Meaningful Timed Models of Closed-Loop DES for Verification Purposes”, Control Engineering Practice, 21:11 (2013), 1620–1639 | DOI

[45] H. M. Hanisch, “Closed-Loop Modeling and Related Problems of Embedded Control Systems in Engineering”, Abstract State Machines 2004. Advances in Theory and Practice, Springer, 2004, 6–19 | DOI | MR

[46] C. Pang, V. Vyatkin, “Systematic Closed-Loop Modelling in IEC 61499 Function Blocks: A Case Study”, IFAC Proceedings Volumes, 42 (2009), 199–204 | DOI

[47] D. Drozdov, S. Patil, V. Dubinin, V. Vyatkin, “Formal Verification of Cyber-Physical Automation Systems Modelled with Timed Block Diagrams”, IEEE Industrial Electronics, 2016, 316–321 | DOI

[48] M. Xavier, S. Patil, V. Vyatkin, “Cyber-Physical Automation Systems Modelling with IEC 61499 for their Formal Verification”, IEEE Industrial Informatics, 2021, 1–6 | DOI

[49] G. Lilli et al, “Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499”, IEEE Open Journal of the Industrial Electronics Society, 4 (2023), 417–431 | DOI

[50] N. Garanina, S. Staroletov, V. Zyubin, I. Anureev, “Model Checking Programs in Process-Oriented IEC 61131-3 Structured Text”, Modeling and Analysis of Information Systems, 31:1 (2024), 32–53 (in Russian) | DOI

[51] N. Halbwachs, F. Lagnier, C. Ratel, “Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE”, IEEE Transactions on Software Engineering, 18:9 (1992), 785–793 | DOI | MR

[52] IEC 61499-1:2012 Function blocks – Part 1: Architecture https://webstore.iec.ch/publication/5506

[53] V. E. Zyubin, A. S. Rozov, I. S. Anureev, N. O. Garanina, V. Vyatkin, “poST: A Process-Oriented Extension of the IEC 61131-3 Structured Text Language”, IEEE Access, 10 (2022), 35 238–35 250 | DOI

[54] N. Halbwachs, P. Caspi, P. Raymond, D. Pilaud, “The Synchronous Data Flow Programming Language LUSTRE”, Proceedings of the IEEE, 79:9 (1991), 1305–1320 | DOI

[55] A. Champion, A. Gurfinkel, and et al, “CoCoSpec: A Mode-Aware Contract Language for Reactive Systems”, Software Engineering and Formal Methods, LNTCS, 9763, Springer, 2016, 347–366 | DOI

[56] A. Benveniste, P. Caspi, and et al, “The Synchronous Languages 12 Years Later”, Proceedings of the IEEE, 91:1 (2003), 64–83 | DOI

[57] A. Bouajjani, J. Fernandez, N. Halbwachs, On the Verification of Safety Properties, Rapport Technique SPECTRE L12, 1990

[58] P. Raymond, “Synchronous Program Verification with Lustre/Lesar”, Modeling and Verification of Real-Time Systems, ch. 6, John Wiley Sons, 2008, 171–206 | DOI

[59] A. Champion, A. Mebsout, C. Sticksel, C. Tinelli, “The Kind 2 Model Checker”, Computer Aided Verification, LNTCS, 9780, Springer, 2016, 510–517 | DOI | MR

[60] N. Halbwachs, Synchronous Programming of Reactive Systems, Springer, 1993 | MR

[61] M. Sirjani, E. A. Lee, E. Khamespanah, “Verification of Cyberphysical Systems”, Mathematics, 8:7 (2020) | DOI

[62] S. Lin et al, “Towards Building Verifiable CPS using Lingua Franca”, ACM Transactions on Embedded Computing Systems, 22:5s (2023), 1–24 | DOI | Zbl

[63] P. Raymond, Y. Roux, E. Jahier, “Lutin: A Language for Specifying and Executing Reactive Scenarios”, EURASIP Journal on Embedded Systems, 2008 (2008), 1–11 | DOI

[64] B. Finkbeiner, “Synthesis of Reactive Systems”, Dependable Software Systems Engineering, 45 (2016), 72–98 | DOI

[65] N. Piterman, A. Pnueli, Y. SaTar, “Synthesis of Reactive (1) Designs”, Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, 3855, Springer, 2006, 364–380 | DOI | MR | Zbl

[66] M. Roth, L. Litz, J. J. Lesage, “Identification of Discrete Event Systems: Implementation Issues and Model Completeness”, Informatics in Control, Automation and Robotics, 3 (2010), 73–80

[67] I. Buzhinsky, V. Vyatkin, “Automatic Inference of Finite-State Plant Models From Traces and Temporal Properties”, IEEE Transactions on Industrial Informatics, 13:4 (2017), 1521–1530 | DOI

[68] P. Ovsiannikova, D. Chivilikhin, V. Ulyantsev, A. Shalyto, “Closed-Loop Verification of a Compensating Group Drive Model Using Synthesized Formal Plant Model”, IEEE Emerging Technologies and Factory Automation, 2017, 1–4 | DOI

[69] I. Buzhinsky, A. Pakonen, V. Vyatkin, “Scalable Methods of Discrete Plant Model Generation for Closed-Loop Model Checking”, IEEE Industrial Electronics Society, 2017, 5483–5488 | DOI

[70] M. Xavier, J. Hakansson, S. Patil, V. Vyatkin, “Plant Model Generator from Digital Twin for Purpose of Formal Verification”, IEEE Emerging Technologies and Factory Automation, 2021, 1–4 | DOI | Zbl

[71] M. Xavier, V. Dubinin, S. Patil, V. Vyatkin, Plant Model Generation From Event Log Using ProM for Formal Verification of CPS, 2022, arXiv: 2211.03681 | DOI | MR

[72] nuXmv User Manual https://nuxmv.fbk.eu/downloads/nuxmv-user-manual.pdf