МОДЕЛИРОВАНИЕ И АНАЛИЗ ИНФОРМАЦИОННЫХ СИСТЕМ

V. E. Zyubin, “Hyper-automaton: a Model of Control Algorithms”, in 2007 Siberian Conference on Control and Communications, 2007, pp. 51-57,. DOI: 10.1109/SIBCON.2007.371297

I. Anureev, N. Garanina, T. Liakh, A. Rozov, V. Zyubin, and S. Gorlatch, “Two-step deductive verification of control software using Reflex”, in International Andrei Ershov Memorial Conference on Perspectives of System Informatics, 2019, pp. 50-63,. DOI: 10.1007/978-3-030-37487-7_5 EDN: JQNCBR

V. E. Zyubin, T. V. Liakh, and A. S. Rozov, “Reflex language: a practical notation for cyber-physical systems”, System Informatics, no. 12, pp. 85-104, 2018. EDN: YQVJRZ

C. Paulin-Mohring, “Introduction to the Coq proof-assistant for practical software verification”, in LASER Summer School on Software Engineering, Springer, 2011, pp. 45-95.

I. Chernenko, I. S. Anureev, N. O. Garanina, and S. M. Staroletov, “A Temporal Requirements Language for Deductive Verification of Process-Oriented Programs”, in IEEE 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), 2022, pp. 657-662,. DOI: 10.1109/EDM55285.2022.9855145 EDN: YCNAAC

I. M. Chernenko and I. S. Anureev, “Development of Verification Condition Generator for Process-Oriented Programs in poST Language”, in IEEE 24th International Conference of Young Professionals in Electron Devices and Materials (EDM), 2023, pp. 1760-1765,. DOI: 10.1109/EDM58354.2023.10225217

PoST: A Process-Oriented Extension of the IEC 61131-3 Structured Text Language / V. E. Zyubin, A. S. Rozov, I. S. Anureev [et al.] // IEEE Access. - 2022. - Vol. 10. - P. 35238-35250. DOI: 10.1109/ACCESS.2022.3157601 EDN: JQKGUE

IEC, “IEC 61131-3: 2013 programmable controllers-Part 3: programming languages”. 2013, [Online]. Available: https://webstore.iec.ch/publication/4552.

L. C. Paulson, T. Nipkow, and M. Wenzel, “From LCF to Isabelle/HOL”, Formal Aspects of Computing, vol. 31, pp. 675-698, 2019.

I. M. Chernenko, "Requirements patterns in deductive verification of process-oriented programs and examples of their use", System Informatics, no. 22, 2023,.  DOI: 10.31144/si.2307-6410.2023.n22.p11-20  EDN: RCVNYY  

J.-C. Filliatre, "Deductive software verification", ˆ International Journal on Software Tools for Technology Transfer, vol. 13, pp. 397-403, 2011.  DOI: 10.1007/s10009-011-0211-0  

D. Gurov, P. Herber, and I. Schaefer, "Automated Verification of Embedded Control Software", in International Symposium on Leveraging Applications of Formal Methods, 2020, pp. 235-239,.  DOI: 10.1007/978-3-030-61467-6_15  

D. Gurov, C. Lidstr"om, M. Nyberg, and J. Westman, "Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report", in Critical Systems: Formal Methods and Automated Verification, 2017, pp. 3-18.  

C. B. Louren\cco, D. Cousineau, F. Faissole, C. March\'e, D. Mentr\'e, and H. Inoue, "Automated Verification of Temporal Properties of Ladder Programs", in Formal Methods for Industrial Critical Systems, 2021, pp. 21-38.  

Z. Manna et al., "An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems", in Tool Support for System Specification, Development and Verification, 1999, pp. 174-188,.  DOI: 10.1007/978-3-7091-6355-9_13  

S. Yamane, "Deductive verification method of real-time safety properties for embedded assembly programs", Electronics, vol. 8, no. 10, p. 1163, 2019.  

E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of model checking. Springer, 2018.  

N. O. Garanina et al., "A Temporal Logic for Programmable Logic Controllers", Automatic Control and Computer Sciences, vol. 55, no. 7, pp. 763-775, 2021,.  DOI: 10.3103/S0146411621070038  EDN: MAMSGN  

Z. Manna and A. Pnueli, The temporal logic of reactive and concurrent systems: Specification. Springer New York, NY, 1992.  

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, "Patterns in Property Specifications for Finite-State Verification", in Proceedings of the 21st International Conference on Software Engineering, 1999, pp. 411-420,.  DOI: 10.1145/302405.302672  

L. Grunske, "Specification patterns for probabilistic quality properties", in Proceedings of the 30th international conference on Software engineering, 2008, pp. 31-40,.  DOI: 10.1145/1368088.1368094  

S. Konrad and B. H. C. Cheng, "Real-Time Specification Patterns", in Proceedings of the 27th International Conference on Software Engineering, 2005, pp. 372-381,.  DOI: 10.1145/1062455.1062526  

A. Mekki, M. Ghazel, and A. Toguy\'eni, "Assisting Temporal Requirement Specification", Computer Technology and Application, vol. 3, no. 1, pp. 47-55, 2012.  

O. Mondragon, A. Q. Gates, and S. Roach, "Prospec: Support for elicitation and formal specification of software properties", Electronic Notes in Theoretical Computer Science, vol. 89, no. 2, pp. 67-88, 2003,.  DOI: 10.1016/S1571-0661(04)81043-0  

S. Salamah, A. Gates, and V. Kreinovich, "Validated Templates for Specification of Complex LTL Formulas", Journal of Systems and Software, vol. 85, no. 8, pp. 1915-1929, 2012,.  DOI: 10.1016/j.jss.2012.02.041  

D. Bianculli, C. Ghezzi, C. Pautasso, and P. Senti, "Specification patterns from research to industry: A case study in service-based applications", in 34th International Conference on Software Engineering (ICSE), 2012, pp. 968-976,.  DOI: 10.1109/ICSE.2012.6227125  

S. Halle, R. Villemaire, and O. Cherkaoui, "Specifying and Validating Data-Aware Temporal Web Service Properties", IEEE Transactions on Software Engineering, vol. 35, no. 5, pp. 669-683, 2009,.  DOI: 10.1109/TSE.2009.29  

A. Post, I. Menzel, and A. Podelski, "Applying Restricted English Grammar on Automotive Requirements-Does it Work? A Case Study", in Requirements Engineering: Foundation for Software Quality, 2011, pp. 166-180.  

M. Autili, L. Grunske, M. Lumpe, P. Pelliccione, and A. Tang, "Aligning Qualitative, Real-Time, and Probabilistic Property Specification Patterns Using a Structured English Grammar", IEEE Transactions on Software Engineering, vol. 41, no. 7, pp. 620-638, 2015,.  DOI: 10.1109/TSE.2015.2398877  

A. N. Getmanova, N. O. Garanina, S. M. Staroletov, V. E. Zyubin, and I. S. Anureev, "Semantic Classification of Event Driven Temporal Logic Requirements", in IEEE 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), 2022, pp. 663-668,.  DOI: 10.1109/EDM55285.2022.9855053  

Event-Driven Temporal Logic Pattern for Control Software Requirements Specification / V. Zyubin, I. Anureev, N. Garanina [et al.] // Lecture Notes in Computer Science. - 2021. - Vol. 12818 LNCS. - P. 92-107.  DOI: 10.1007/978-3-030-89247-0_7  EDN: SNXHVN