Н. О. Гаранина, И. С. Ануреев, В. Е. Зюбин, С. М. Старолетов, Т. В. Лях, А. С. Розов, С. П. Горлач
|
|
|
Список литературы
|
|
|
1. |
I. Anureev, “Operacionnaya semantica annotirovannih Re-ex programm”, Modelirovanie i analiz informacionnyh sistem, 26:6 (2019), 181–192 |
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 |
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 |
5. |
A. Mader, “A Classification of PLC Models and Applications”, Discrete Event Systems, SECS, 569, Springer, 2000, 239–246 |
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 |
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 |
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 |
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 |
13. |
T. Ovatman, “An overview of model checking practices on verification of PLC Software”, Software & Systems Modeling, 4:15 (2016), 937–960 |
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 |
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 |
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 |
19. |
O. Ljungkrantz, “An empirical study of control logic specifications for programmable logic controllers”, Empirical Software Engineering, 3:19 (2014), 655–677 |
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 |
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 |