References

mais

Моделирование и анализ информационных систем

Modeling and Analysis of Information Systems

1818-10152313-5417

Yaroslavl State University

10.18255/1818-1015-2024-3-240-279

mais-1877

Research Article

Theory of Software

LTL-спецификация для разработки и верификации программ логического управления в системах с обратной связью

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

https://orcid.org/0009-0000-6893-6137

Нейзов

Максим Вячеславович

Neyzov

Maxim V.

neyzov.max@gmail.com

https://orcid.org/0000-0003-0500-306X

Кузьмин

Егор Владимирович

Kuzmin

Egor V.

kuzmin@uniyar.ac.ru

Институт автоматики и электрометрии СО РАНРоссияInstitute of Automation and Electrometry SB RASRussian Federation

Ярославский государственный университет им. П.Г. ДемидоваРоссияP.G. Demidov Yaroslavl State UniversityRussian Federation

2024

13092024

313240279

2024

Нейзов М.В., Кузьмин Е.В.

Neyzov M.V., Kuzmin E.V.

Данная работа распространяется под лицензией Creative Commons Attribution 4.0.

This work is licensed under a Creative Commons Attribution 4.0 License.

https://www.mais-journal.ru/jour/article/view/1877

Статья продолжает цикл публикаций по разработке и верификации управляющих программ на основе LTL-спецификаций специального вида. Ранее для описания строго детерминированного поведения программ была предложена декларативная LTL-спецификация, проработаны способы её верификации и трансляции: для верификации используется инструмент проверки модели nuXmv, трансляция осуществляется в императивный язык программирования ST для программируемых логических контроллеров. При верификации декларативной LTL-спецификации поведения программ может возникнуть необходимость в моделировании поведения её окружения. В общем случае требуется обеспечить возможность построения замкнутых систем «программа-окружение». В настоящей работе для описания поведения окружения программ логического управления предложена LTL-спецификация ограниченно недетерминированного поведения булевой переменной. Данная спецификация позволяет задавать поведение булевых сигналов обратной связи, а также условия справедливости для исключения нереалистичных сценариев поведения. В статье предлагается подход к разработке и верификации программ логического управления, в рамках которого модель поведения окружения программы описывается в виде ограничений на поведение её входных сигналов, что позволяет избежать отдельного детального представления процессов функционирования окружения. В результате полученная модель поведения замкнутой системы «программа-окружение» даёт ряд преимуществ: упрощение процесса моделирования, сокращение пространства состояний проверяемой модели, снижение времени верификации. При невозможности сведения поведения окружения к поведению имеющихся входных сигналов данный подход предполагает применение «мнимых» датчиков — дополнительных булевых переменных, использующихся как вспомогательное средство для описания поведения входных сигналов. Цель введения мнимых датчиков состоит в компенсации недостающих датчиков для отслеживания специфического поведения отдельных элементов окружения, которое необходимо учесть при задании реалистичного поведения входов программы логического управления. Предложенный подход к разработке и верификации программ с учётом поведения окружения (объекта управления) демонстрируется на примере промышленной установки для литья пластмасс.

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 non\-de\-ter\-mi\-nis\-tic 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.

управляющее программное обеспечениеПЛК-программадекларативная LTL-спецификацияLTL-спецификация ограниченно недетерминированного поведенияусловия справедливостиверификация замкнутых системмодель поведения установкимнимый датчиктемпоральные свойствапроверка моделиверификатор nuXmvSMV-спецификация

control softwarePLC programdeclarative LTL-specificationLTL-specification of constraintly nondeterministic behaviorfairness conditionsclosed-loop systems verificationplant behavior modelimaginary sensortemporal propertiesmodel checkingnuXmv verifierSMV-specification

Госзадание ИАиЭ СО РАН, проект No 122031600173-8; ЯрГУ (проект VIP-016).

State task IAaE SB RAS, project No. 122031600173-8; Yaroslavl State University (project VIP-016).

References1

S. Oks and et al., “Cyber-Physical Systems in the Context of Industry 4.0: A Review, Categorization and Outlook,” Information Systems Frontiers, pp. 1–42, 2022, doi: 10.1007/s10796-022-10252-x.

K. Zhang, Y. Shi, S. Karnouskos, T. Sauter, H. Fang, and A. W. Colombo, “Advancements in Industrial Cyber-Physical Systems: An Overview and Perspectives,” IEEE Transactions on Industrial Informatics, vol. 19, no. 1, pp. 716–729, 2023, doi: 10.1109/TII.2022.3199481.

S. J. Oks, Industrial Cyber-Physical Systems: Advancing Industry 4.0 from Vision to Application, 1st ed. Springer, 2024.

C. Dey and S. K. Sen, Industrial Automation Technologies, 1st ed. CRC Press, 2020.

K. Thramboulidis, “A Cyber–Physical System-Based Approach for Industrial Automation Systems,” Computers in Industry, vol. 72, pp. 92–102, 2015, doi: 10.1016/j.compind.2015.04.006.

“IEC 61131-1:2003 Programmable controllers -- Part 1: General information.” [Online]. Available: https://webstore.iec.ch/publication/4550.

R. Langmann and L. F. Rojas-Peña, “A PLC as an Industry 4.0 Component,” in Remote Engineering and Virtual Instrumentation, 2016, pp. 10–15, doi: 10.1109/REV.2016.7444433.

D. Harel and A. Pnueli, “On the Development of Reactive Systems,” in Logics and Models of Concurrent Systems, 1985, vol. 13, pp. 477–498, doi: 10.1007/978-3-642-82453-1_17.

A. Maurya and D. Kumar, “Reliability of safety‐critical systems: A state‐of‐the‐art review,” Quality and Reliability Engineering International, vol. 36, Aug. 2020, doi: 10.1002/qre.2715.

D. J. Smith and K. G. L. Simpson, The Safety Critical Systems Handbook, 5th ed. Butterworth-Heinemann, 2020.

V. Vyatkin, “Software Engineering in Industrial Automation: State-of-the-Art Review,” IEEE Transactions on Industrial Informatics, vol. 9, no. 3, pp. 1234–1249, 2013, doi: 10.1109/TII.2013.2258165.

S. Mitra, Verifying Cyber-Physical Systems: A Path to Safe Autonomy. MIT Press, 2021.

V. D'Silva, D. Kroening, and G. Weissenbacher, “A Survey of Automated Techniques for Formal Software Verification,” in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2008, vol. 27, no. 7, pp. 1165–1178, doi: 10.1109/TCAD.2008.923410.

R. Sinha, S. Patil, L. Gomes, and V. Vyatkin, “A Survey of Static Formal Methods for Building Dependable Industrial Automation Systems,” IEEE Transactions on Industrial Informatics, vol. 15, no. 7, pp. 3772–3783, 2019, doi: 10.1109/TII.2019.2908665.

E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st ed., vol. 10. Springer, 2018.

Y. G. Karpov, MODEL CHECKING. Verification of Parallel and Distributed Program Systems. BHV-Peterburg, 2010, p. 560.

E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002, p. 416.

A. Pnueli, “Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends,” in Current Trends in Concurrency, 1986, vol. 224, pp. 510–584, doi: 10.1007/BFb0027047.

K. Schneider, J. Shabolt, and J. G. Taylor, Verification of reactive systems: formal methods and algorithms, 1st ed. Springer, 2004.

Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety, 1st ed. Springer, 2012.

J. Galv ao, C. Oliveira, and et al., “Formal Verification: Focused on the Verification Using a Plant Model,” in Innovation, Engineering and Entrepreneurship, 2019, pp. 124–131, doi: 10.1007/978-3-319-91334-6_18.

G. Frey and L. Litz, “Formal Methods in PLC Programming,” in IEEE International Conference On Systems, Man and Cybernetics, 2000, vol. 4, pp. 2431–2436, doi: 10.1109/ICSMC.2000.884356.

J. M. Machado, B. Denis, and et al., “Logic Controllers Dependability Verification Using a Plant Model,” IFAC Proceedings Volumes, vol. 39, no. 17, pp. 37–42, 2006, doi: 10.3182/20060926-3-PL-4904.00007.

A. A. Shalyto, “Logic Control and ‘Reactive’ Systems: Algorithmization and Programming,” Automation and Remote Control, vol. 62, no. 1, pp. 1–29, 2001, doi: 10.1023/A:1002837232103.

E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors,” Modeling and Analysis of Information Systems, vol. 21, no. 4, pp. 75–90, 2014, doi: 10.18255/1818-1015-2014-4-75-90.

E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors,” Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 602–614, 2014, doi: 10.3103/S0146411614070256.

M. V. Neyzov and E. V. Kuzmin, “LTL-specification for Development and Verification of Control Programs,” Modeling and Analysis of Information Systems, vol. 30, no. 4, pp. 308–339, 2023, doi: 10.18255/1818-1015-2023-4-308-339.

M. V. Neyzov and E. V. Kuzmin, “Verification of Declarative LTL-specification of Control Programs Behavior,” Modeling and Analysis of Information Systems, vol. 31, no. 2, pp. 120–141, 2024, doi: 10.18255/1818-1015-2024-2-120-141.

“nuXmv Home.” [Online]. Available: https://nuxmv.fbk.eu/.

M. Frappier, B. Fraikin, R. Chossart, R. Chane-Yack-Fa, and M. Ouenzar, “Comparison of Model Checking Tools for Information Systems,” in Formal Methods and Software Engineering, 2010, vol. 6447, pp. 581–596, doi: 10.1007/978-3-642-16901-4_38.

“Spot Home.” [Online]. Available: https://spot.lre.epita.fr/.

M. Xavier, S. Patil, V. Dubinin, and V. Vyatkin, “Formal Modelling, Analysis, and Synthesis of Modular Industrial Systems Inspired by Net Condition/Event Systems,” in Applications and Theory of Petri Nets and Concurrency, 2023, pp. 16–33, doi: 10.1007/978-3-031-33620-1_2.

S. Patil, S. Bhadra, and V. Vyatkin, “Closed-Loop Formal Verification Framework with Non-Determinism, Configurable by Meta-Modelling,” in IEEE Industrial Electronics Society, 2011, pp. 3770–3775, doi: 10.1109/IECON.2011.6119923.

S. Patil, V. Vyatkin, and M. Sorouri, “Formal Verification of Intelligent Mechatronic Systems with Decentralized Control Logic,” in IEEE Emerging Technologies & Factory Automation, 2012, pp. 1–7, doi: 10.1109/ETFA.2012.6489678.

S. Patil, V. Vyatkin, and C. Pang, “Counterexample-Guided Simulation Framework for Formal Verification of Flexible Automation Systems,” in IEEE Industrial Informatics, 2015, pp. 1192–1197, doi: 10.1109/INDIN.2015.7281905.

C. Gerber, S. Preuße, and H.-M. Hanisch, “A Complete Framework for Controller Verification in Manufacturing,” in IEEE Emerging Technologies & Factory Automation, 2010, pp. 1–9, doi: 10.1109/ETFA.2010.5641220.

S. Preuße, H.-C. Lapp, and H.-M. Hanisch, “Closed-Loop System Modeling, Validation, and Verification,” in IEEE Emerging Technologies & Factory Automation, 2012, pp. 1–8, doi: 10.1109/ETFA.2012.6489679.

J. Machado, B. Denis, and J.-J. Lesage, “A Generic Approach to Build Plant Models for DES Verification Purposes,” in International Workshop on Discrete Event Systems, 2006, pp. 407–412, doi: 10.1109/WODES.2006.382508.

J. Machado, E. Seabra, and et al., “Safe Controllers Design for Industrial Automation Systems,” Computers & Industrial Engineering, vol. 60, no. 4, pp. 635–653, 2011, doi: 10.1016/j.cie.2010.12.020.

M. Perin and J.-M. Faure, “Building Meaningful Timed Models of Closed-Loop DES for Verification Purposes,” Control Engineering Practice, vol. 21, no. 11, pp. 1620–1639, 2013, doi: 10.1016/j.conengprac.2012.05.002.

V. Vyatkin, H.-M. Hanisch, C. Pang, and 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), vol. 39, no. 1, pp. 17–28, 2009, doi: 10.1109/TSMCC.2008.2005785.

A. Lobov, J. L. M. Lastra, and R. Tuokko, “Application of UML in Plant Modeling for Model-Based Verification: UML Translation to TNCES,” in IEEE Industrial Informatics, 2005, pp. 495–501, doi: 10.1109/INDIN.2005.1560426.

A. Lobov, J. L. M. Lastra, and R. Tuokko, “On Controller and Plant Modeling for Model-Based Formal Verification,” in IEEE Emerging Technologies and Factory Automation, 2005, vol. 1, pp. 121–128, doi: 10.1109/ETFA.2005.1612510.

S. Preusse, Technologies for Engineering Manufacturing Systems Control in Closed Loop, 10th ed. Logos Verlag Berlin GmbH, 2013.

H.-M. Hanisch, “Closed-Loop Modeling and Related Problems of Embedded Control Systems in Engineering,” in Abstract State Machines 2004. Advances in Theory and Practice, 2004, pp. 6–19, doi: 10.1007/978-3-540-24773-9_2.

C. Pang and V. Vyatkin, “Systematic Closed-Loop Modelling in IEC 61499 Function Blocks: A Case Study,” IFAC Proceedings Volumes, vol. 42, pp. 199–204, 2009, doi: 10.3182/20090603-3-RU-2001.0264.

D. Drozdov, S. Patil, V. Dubinin, and V. Vyatkin, “Formal Verification of Cyber-Physical Automation Systems Modelled with Timed Block Diagrams,” in IEEE Industrial Electronics, 2016, pp. 316–321, doi: 10.1109/ISIE.2016.7744910.

M. Xavier, S. Patil, and V. Vyatkin, “Cyber-Physical Automation Systems Modelling with IEC 61499 for their Formal Verification,” in IEEE Industrial Informatics, 2021, pp. 1–6, doi: 10.1109/INDIN45523.2021.9557416.

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, vol. 4, pp. 417–431, 2023, doi: 10.1109/OJIES.2023.3321084.

N. O. Garanina, S. M. Staroletov, V. E. Zyubin, and I. S. Anureev, “Model Checking Programs in Process-Oriented IEC 61131-3 Structured Text,” Modeling and Analysis of Information Systems, vol. 31, no. 1, pp. 32–53, 2024, doi: 10.18255/1818-1015-2024-1-32-53.

N. Halbwachs, F. Lagnier, and C. Ratel, “Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE,” IEEE Transactions on Software Engineering, vol. 18, no. 9, pp. 785–793, 1992, doi: 10.1109/32.159839.

“IEC 61499-1:2012 Function blocks -- Part 1: Architecture.” [Online]. Available: https://webstore.iec.ch/publication/5506.

V. E. Zyubin, A. S. Rozov, I. S. Anureev, N. O. Garanina, and V. Vyatkin, “poST: A Process-Oriented Extension of the IEC 61131-3 Structured Text Language,” IEEE Access, vol. 10, pp. 35238–35250, 2022, doi: 10.1109/ACCESS.2022.3157601.

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, “The Synchronous Data Flow Programming Language LUSTRE,” Proceedings of the IEEE, vol. 79, no. 9, pp. 1305–1320, 1991, doi: 10.1109/5.97300.

A. Champion, A. Gurfinkel, and et al., “CoCoSpec: A Mode-Aware Contract Language for Reactive Systems,” in Software Engineering and Formal Methods, 2016, vol. 9763, pp. 347–366, doi: 10.1007/978-3-319-41591-8_24.

A. Benveniste, P. Caspi, and et al., “The Synchronous Languages 12 Years Later,” Proceedings of the IEEE, vol. 91, no. 1, pp. 64–83, 2003, doi: 10.1109/JPROC.2002.805826.

A. Bouajjani, J. C. Fernandez, and N. Halbwachs, “On the Verification of Safety Properties,” Rapport Technique SPECTRE L12, 1990.

P. Raymond, “Synchronous Program Verification with Lustre/Lesar,” in Modeling and Verification of Real‐Time Systems, John Wiley & Sons, 2008, pp. 171–206.

A. Champion, A. Mebsout, C. Sticksel, and C. Tinelli, “The Kind 2 Model Checker,” in Computer Aided Verification, 2016, vol. 9780, pp. 510–517, doi: 10.1007/978-3-319-41540-6_29.

N. Halbwachs, Synchronous Programming of Reactive Systems. Springer, 1993.

M. Sirjani, E. A. Lee, and E. Khamespanah, “Verification of Cyberphysical Systems,” Mathematics, vol. 8, no. 7, 2020, doi: 10.3390/math8071068.

S. Lin et al., “Towards Building Verifiable CPS using Lingua Franca,” ACM Transactions on Embedded Computing Systems, vol. 22, no. 5s, pp. 1–24, 2023, doi: 10.1145/3609134.

P. Raymond, Y. Roux, and E. Jahier, “Lutin: A Language for Specifying and Executing Reactive Scenarios,” EURASIP Journal on Embedded Systems, vol. 2008, pp. 1–11, 2008, doi: 10.1155/2008/753821.

B. Finkbeiner, “Synthesis of Reactive Systems,” Dependable Software Systems Engineering, vol. 45, pp. 72–98, 2016, doi: 10.3233/978-1-61499-627-9-72.

N. Piterman, A. Pnueli, and Y. Sa’ar, “Synthesis of Reactive (1) Designs,” in Verification, Model Checking, and Abstract Interpretation, 2006, vol. 3855, pp. 364–380, doi: 10.1007/11609773_24.

M. Roth, L. Litz, and J.-J. Lesage, “Identification of Discrete Event Systems: Implementation Issues and Model Completeness,” in Informatics in Control, Automation and Robotics, 2010, vol. 3, pp. 73–80.

I. Buzhinsky and V. Vyatkin, “Automatic Inference of Finite-State Plant Models From Traces and Temporal Properties,” IEEE Transactions on Industrial Informatics, vol. 13, no. 4, pp. 1521–1530, 2017, doi: 10.1109/TII.2017.2670146.

P. Ovsiannikova, D. Chivilikhin, V. Ulyantsev, and A. Shalyto, “Closed-Loop Verification of a Compensating Group Drive Model Using Synthesized Formal Plant Model,” in IEEE Emerging Technologies and Factory Automation, 2017, pp. 1–4, doi: 10.1109/ETFA.2017.8247714.

I. Buzhinsky, A. Pakonen, and V. Vyatkin, “Scalable Methods of Discrete Plant Model Generation for Closed-Loop Model Checking,” in IEEE Industrial Electronics Society, 2017, pp. 5483–5488, doi: 10.1109/IECON.2017.8216949.

M. Xavier, J. Håkansson, S. Patil, and V. Vyatkin, “Plant Model Generator from Digital Twin for Purpose of Formal Verification,” in IEEE Emerging Technologies and Factory Automation, 2021, pp. 1–4, doi: 10.1109/ETFA45728.2021.9613704.

M. Xavier, V. Dubinin, S. Patil, and V. Vyatkin, “Plant Model Generation From Event Log Using ProM for Formal Verification of CPS,” arXiv preprint arXiv:2211.03681, 2022, doi: 10.48550/arXiv.2211.03681.

“nuXmv User Manual.” [Online]. Available: https://nuxmv.fbk.eu/downloads/nuxmv-user-manual.pdf.

The authors declare that there are no conflicts of interest present.