Preview

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

Расширенный поиск

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

https://doi.org/10.18255/1818-1015-2024-3-240-279

Аннотация

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

Об авторах

Максим Вячеславович Нейзов
Институт автоматики и электрометрии СО РАН
Россия


Егор Владимирович Кузьмин
Ярославский государственный университет им. П.Г. Демидова
Россия


Список литературы

1. 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.

2. 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.

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

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

5. 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.

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

7. 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.

8. 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.

9. 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.

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

11. 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.

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

13. 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.

14. 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.

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

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

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

18. 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.

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

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

21. 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.

22. 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.

23. 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.

24. 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.

25. 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.

26. 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.

27. 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.

28. 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.

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

30. 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.

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

32. 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.

33. 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.

34. 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.

35. 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.

36. 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.

37. 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.

38. 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.

39. 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.

40. 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.

41. 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.

42. 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.

43. 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.

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

45. 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.

46. 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.

47. 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.

48. 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.

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

50. 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.

51. 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.

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

53. 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.

54. 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.

55. 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.

56. 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.

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

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

59. 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.

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

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

62. 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.

63. 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.

64. 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.

65. 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.

66. 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.

67. 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.

68. 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.

69. 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.

70. 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.

71. 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.

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


Рецензия

Для цитирования:


Нейзов М.В., Кузьмин Е.В. LTL-спецификация для разработки и верификации программ логического управления в системах с обратной связью. Моделирование и анализ информационных систем. 2024;31(3):240-279. https://doi.org/10.18255/1818-1015-2024-3-240-279

For citation:


Neyzov M.V., Kuzmin E.V. LTL-specification for development and verification of logical control programs in feedback systems. Modeling and Analysis of Information Systems. 2024;31(3):240-279. (In Russ.) https://doi.org/10.18255/1818-1015-2024-3-240-279

Просмотров: 313


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)