RUS  ENG
Полная версия
ЖУРНАЛЫ // Моделирование и анализ информационных систем

Модел. и анализ информ. систем, 2020, том 27, номер 4, страницы 412–427 (Mi mais725)

Темпоральная логика для программируемых логических контроллеров
Н. О. Гаранина, И. С. Ануреев, В. Е. Зюбин, С. М. Старолетов, Т. В. Лях, А. С. Розов, С. П. Горлач

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

1. I. Anureev, “Operacionnaya semantica annotirovannih Re-ex programm”, Modelirovanie i analiz informacionnyh sistem, 26:6 (2019), 181–192  mathscinet
2. I. Anureev, N. Garanina, T. Liakh, A. Rozov, V. Zyubin, “Towards safe cyber-physical systems: the Reflex language and its transformational semantics”, IEEE International Siberian Conference on Control and Communications, IEEE, 2019, 18–20
3. E. Brinksma, A. Mader, “Verification and Optimization of a PLC Control Schedule”, SPIN Model Checking and Software Verification, SPIN 2000, LNCS, 1885, Springer, 2000, 73–92  zmath
4. V. Gourcuff, O. de Smet, J. M. Faure, “Improving large-sized PLC programs verification using abstractions”, IFAC Proceedings Volumes, 41:2 (2008), 5101–5106  crossref
5. A. Mader, “A Classification of PLC Models and Applications”, Discrete Event Systems, SECS, 569, Springer, 2000, 239–246  mathscinet
6. H. Wan, G. Chen, X. Song, M. Gu, “Formalization and Verification of PLC Timers in Coq”, Proc. of 33rd Annual IEEE International Computer Software and Applications Conference, IEEE, 2009, 315–323
7. J. Yoo, S. Cha, E. Jee, “A Verification Framework for FBD Based Software in Nuclear Power Plants”, Proc. of 15th Asia-Pacific Software Engineering Conference, IEEE, 2008, 385–392
8. D. Bulavskij, V. Zyubin, N. Karlson, V. Krivoruchko, V. Mironov, “An Automated Control System for a Silicon Single-Crystal Growth Furnace”, Optoelectronics, instrumentation, and data processing, 32:2 (1996), 25–30
9. P. G. Kovadlo, A. Lubkov, A. Bevzov, and et al, “Automation system for the large solar vacuum telescope”, Optoelectronics, Instrumentation and Data processing, 52 (2016), 187–195  crossref
10. A. Gupta, V. Kahlon, S. Qadeer, T. Touili, “Model Checking Concurrent Programs”, Handbook of Model Checking, ch. 18, Springer International Publishing, 2018, 573–577  crossref  mathscinet
11. E. M. Clarke, T. A. Henzinger, H. Veith, “Introduction to Model Checking”, Handbook of Model Checking, ch. 1, Springer International Publishing, 2018, 1–13  mathscinet
12. H. Dierks, “PLC-automata: A new class of implementable real-time automata”, International AMAST Workshop on Aspects of Real-Time Systems and Concurrent and Distributed Software, Lecture Notes in Computer Science, 1231, Springer, 1997, 111–125  crossref
13. T. Ovatman, “An overview of model checking practices on verification of PLC Software”, Software & Systems Modeling, 4:15 (2016), 937–960  crossref
14. E. Kuzmin, D. Ryabukhin, V. A. Sokolov, “On the expressiveness of the approach to constructing PLC-programs by LTL-specification”, Automatic Control and Computer Sciences, 7:50 (2016), 510–519  crossref  mathscinet
15. M. Zhang, “Towards automated safety vetting of PLC code in real-world plants”, IEEE Symposium on Security and Privacy, IEEE, 2019, 522–538
16. A. Rajeev, T. Henzinger, “A really temporal logic”, Journal of the ACM, 41:1 (1994), 181–203  crossref  mathscinet
17. J. Xiong, “A User-Friendly Verification Approach for IEC 61131-3 PLC Programs”, Electronics, 4:9 (2020)
18. B. Beckert, “Regression verification for programmable logic controller software”, International Conference on Formal Engineering Methods, 9407, Lecture Notes in Computer Science, Springer, 2015  mathscinet
19. O. Ljungkrantz, “An empirical study of control logic specifications for programmable logic controllers”, Empirical Software Engineering, 3:19 (2014), 655–677  crossref
20. O. Ljungkrantz, K. Akesson, M. Fabian, C. Yuan, “A formal specification language for PLC-based control logic”, 8th IEEE International Conference on Industrial Informatics, IEEE, 2010, 1067–1072
21. O. Maler, D. Nickovic, “Monitoring temporal properties of continuous signals”, Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, 2004, 152–166  crossref  zmath
22. N. Garanina, I. Anureev, V. Zyubin, A. Rozov, T. Liakh, S. Gorlatch, “Reasoning about Programmable Logic Controllers”, System Informatics, 17 (2020), 33–42
23. G. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003


© МИАН, 2025