Russian Federation
Smolensk, Smolensk, Russian Federation
UDC 004.415.5
UDC 004.415.52
UDC 004.415.53
UDC 62
The relevance of the chosen topic stems from the growing requirements for the reliability of special software (SW) in multiprocessor computing systems of tactical-level automated control complexes (KS AU). In modern military operations, such systems face high loads, including parallel processes and strict real-time requirements, where even a single defect can lead to critical failures. Verification serves as a key means to ensure defect-free operation, minimizing risks and enhancing resilience to external threats. The research aims to develop a comprehensive verification methodology for special SW in multiprocessor KS AU systems at the tactical level, guaranteeing defect-free performance across all lifecycle stages—from design to operation. This methodology integrates formal verification methods (model checking), dynamic testing, and cyberimmunity criteria tailored to the specifics of tactical-level control. The scientific novelty lies in the proposed approach combining static model analysis with real-time integrity monitoring of SW in a multiprocessor environment. Unlike traditional methods, the new methodology accounts for the specifics of inter-processor exchange and distributed computing in KS AU, introducing quantifiable verification criteria for acquired cyberimmunity. The practical significance is evident in the potential for direct implementation of the developed methods to enhance the reliability of existing tactical-level KS AU systems, aligning with GOST R 51901.3-2002 standards and reducing operational risks in combat systems. Application will shorten debugging time and improve overall combat readiness of the complexes. Prospects for application include integration into domestic platforms such as the Elbrus architecture, as well as adaptation for other military computing systems with stringent real-time requirements, contributing to the further development of automated control systems
software verification, defect-free operation, multiprocessor computing systems, automated control complexes, tactical-level KS AU, formal verification methods, cyberimmunity, model checking, dynamic testing, special software
1. Abramov S.M. Methods of ensuring cyberimmunity of special software in automated military systems : PhD thesis (Tech. Sc.). Smolensk, 2023. 156 p.
2. Baier C., Katoen J.-P. Principles of Model Checking. Cambridge : MIT Press, 2008. 954 p.
3. GOST R 51901.3-2002. Reliability in engineering. Software for technological process control. Control and diagnostic methods. Approved 01.07.2003. Moscow : Standartinform, 2002. 28 p.
4. Zdiuruk D.A. Mechanism for control and recovery of special software integrity in multiprocessor computing systems of military purpose based on acquired cyberimmunity / D.A. Zdiuruk, A.N. Neustroev, E.R. Marchenkova // Best Scientific Research 2025: Proceedings of the XXIII International Research Competition, Penza, September 15, 2025. – Penza: Nauka i Prosveshchenie (IP Gulyaev G.Yu.), 2025. – P. 16-20.
5. Zhuravlev Yu.P. Automated tactical-level control systems: Textbook. Smolensk : VA PVO, 2022. 245 p.
6. Kozlov A.S. Hardware-software methods for software protection in multiprocessor computing complexes // Information Technology Security. 2025. Vol. 32, no. 1. P. 78-89.
7. Cuoq P., Kirchner C., Kosmatov N. et al. Frama-C: A software analysis perspective // Software Testing, Verification and Reliability. 2012. Vol. 25, no. 3. P. 229-264.
8. Marchenkova E.R. Verification of multiprocessor computing systems / E.R. Marchenkova // Energy, Informatics, Innovations - 2024 (mathematical modeling and information technologies in production and construction, microelectronics and optotechnics): Proceedings of the XIV International Scientific-Technical Conference, Smolensk, November 13-14, 2024. – Smolensk: [b.i.], 2024. – P. 96-99.
9. Holzmann G.J. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003. 608 p. EDN: https://elibrary.ru/DDRPKD
10. IEEE Std 1012-2016. Standard for System, Software, and Hardware Verification and Validation. New York : IEEE, 2017. 387 p.
11. Owre S., Rushby J., Shankar N. PVS: A Prototype Verification System // 11th International Conference on Automated Deduction (CADE). Saratoga, 1992. P. 748-752. DOI: https://doi.org/10.1007/3-540-55602-8_217; EDN: https://elibrary.ru/MOGUZJ
12. Rutkovsky V.E. Formal verification of parallel programs in real-time systems // Software Products and Systems. 2024. No. 2. P. 34-42.
13. Frolov A.V., Ryzhov V.I. Development of software complex for verification of multiprocessor control systems // News of Higher Educational Institutions. Instrumentation Series. 2018. Vol. 61, no. 5. P. 112-120.
