Стратифікована модель подання нефункціональних характеристик системи критичного призначення при проєктуванні

В.В. Шкарупило ¹, канд. техн. наук, В.В. Душеба ², канд. техн. наук,
С.Ю. Скрупський ³, канд. техн. наук, І.В. Блінов ⁴, д-р техн. наук
¹ Інститут проблем моделювання в енергетиці ім. Г.Є. Пухова НАН України
Україна, 03164, Київ, вул. Генерала Наумова, 15
Національний університет біоресурсів і природокористування України,
Україна, 03041, м. Київ, вул. Героїв Oборони, 15
тел.: +38 (066) 1297345; e-mail: Ця електронна адреса захищена від спам-ботів. Вам необхідно увімкнути JavaScript, щоб побачити її.;
² Інститут проблем моделювання в енергетиці ім. Г.Є. Пухова НАН України
тел.: +38 (050) 4133988; e-mail: Ця електронна адреса захищена від спам-ботів. Вам необхідно увімкнути JavaScript, щоб побачити її.;
³ Національний Університет «Запорізька політехніка» МОН України
Україна, 69063, м. Запоріжжя, вул. Жуковського, 64
тел.: +38 (061) 7698249; e-mail: Ця електронна адреса захищена від спам-ботів. Вам необхідно увімкнути JavaScript, щоб побачити її.;
⁴ Інститут електродинаміки НАН України
Україна, 03057, м. Київ, просп. Перемоги, 56
тел.: +38 (044) 3662443; e-mail: Ця електронна адреса захищена від спам-ботів. Вам необхідно увімкнути JavaScript, щоб побачити її.

Èlektron. model. 2022, 44(2):90-106

https://doi.org/10.15407/emodel.44.02.090

АНОТАЦІЯ

Проєктування — це етап процесу розроблення, який подається у наступній послідов­нос­ті: аналіз вимог до розроблюваної системи, проєктування, реалізація і валідація, яка може бути здійснена за допомогою імітаційного моделювання або тестування. Система критичного призначення — це система, в якій збої і відмови у роботі призводять до критичних наслідків. Використано поняття «артефакт», тобто сутність, що характеризується архітектурою і змістом. Результат виконання певного кроку на етапі проєктування нада­но у вигляді блок-схеми алгоритму, діаграми та формалізованого подання. На етапі проєктування процесу розроблення за даними артефактами здійснюється контроль показників не лише функціональних характеристик (ФХ), а й нефункціональних характеристик (НФХ), які типово перевіряються на заключному етапі валідації процесу розроблення. Проведення контролю при цьому сприяє підвищенню рівня функційної безпечності роз­роблюваної системи з позиції програмно-алгоритмічної складової. Пропонується сприяти цьому через реалізацію механізму спадковості артефактів. Артефакти, несуперечність яких розглянуто і підтверджено як показник ФХ на етапі проєктування процесу розроблення, позиціонуються як вихідні конструкції, на основі яких синтезуються похідні від них артефакти, а саме формалізовані подання, тобто засоби контролю показників НФХ. Для синтезу таких засобів запропоновано ієрархічну модель подання НФХ, яка є засобом уні­фікації, за допомогою якого виконується контроль показників НФХ на етапі проєкту­вання процесу розроблення. Для цього залучено математичний апарат Discrete Event System Specification Бернарда Зейглера.

КЛЮЧОВІ СЛОВА:

Discrete Event System Specification, артефакт, нефункціональні характеристики, проєктування, система критичного призначення.

СПИСОК ЛІТЕРАТУРИ

1. Knight J.C. Safety Critical Systems: Challenges and Directions. Proceedings of the 24th International Conference on Software Engineering, ICSE '02 (Orlando, Florida, May 19-25, 2002). P. 547-550. DOI: https://doi.org/10.1145/581339.581406
2. Shkarupylo V.V., Kudermetov R.K., Polska O.V. On the approaches to cyber-physical systems simulation // Advances in Cyber-Physical Systems (ACPS), 2018, 3, No. 1, рр. 51—54. DOI: https://doi.org/10.23939/acps2018.01.051
3. Интеллектуальные электроэнергетические системы: элементы и режимы / Под общ. ред. акад. НАН Украины А.В. Кириленко. Киев: Ин-т электродинамики НАН Украины, 2014, 408 с.
4. Кириленко О.В., Блінов І.В., Танкевич С.Є. Smart Grid та організація інформаційного обміну в електроенергетичних системах // Технічна електродинаміка, 2012, № 3, с. 47—48.
5. ІEC/TR 63097:2017 Smart grid standardization roadmap. 315 p. URL: https:// standards.iteh.ai/catalog/standards/iec/f3bffb16-2681-4e9f-890a-d63ed6c010cf/iec-tr-63097-2017 (дата звернення: 10.04.2022).
6. Ding D., Han Q.-L., Wang Z., Ge X. A Survey on Model-Based Distributed Control and Filtering for Industrial Cyber-Physical Systems // IEEE Transactions on Industrial Informatics, 2019, 15, No 5, рр. 2483—2499. DOI: https://doi.org/10.1109/TII.2019. 2905295.
7. Resch S., Paulitsch M. Using TLA+ in the Development of a Safety-Critical Fault-Tolerant Middleware. Software Reliability Engineering Workshops: Proc. 2017 IEEE International Symposium (Toulouse, France, 23-26 October 2017). рр. 146—152. DOI: https://doi.org/10.1109/ISSREW.2017.43.
8. Lamport L. Specifying systems: The TLA+ language and tools for hardware and software engineers. Boston : Addison-Wesley, 2002, 382 р.
9. CENELEC - EN 50128.Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems, by European Committee for Electrotechnical Standardization (CENELEC), June 2020. URL: https://standards. com/std/14317747/EN%2050128 (дата звернення: 12.04.2021).
10. Наказ Державної інспекції ядерного регулювання від 22.07.2015 № 140 із змінами, внесеними згідно з Наказом Державної інспекції ядерного регулювання № 508 від 11.2019. URL: https://zakon.rada.gov.ua/laws/term/34229 (дата звернення: 21.03.2022).
11. Broy M. A logical approach to systems engineering artifacts and traceability: from requirements to functional and architectural views. Engineering dependable software systems: NATO Science for Peace and Security Series - D: Information and Communication Security / Еds. M. Broy, D. Peled, G. Kalus // IOS Press, 2013, 34, рр. 1—48. DOI: https://doi.org/10.3233/978-1-61499-207-3-1.
12. Шкарупило В.В., Блінов І.В. Сценарії, методи та засоби формальної верифікації артефактів процесу проєктування систем критичного призначення. Вінниця: ГО «Європейська наукова платформа», 2021, 104 с. DOI: https://doi.org/10.36074/ smtzfvappskp-monograph.2021.
13. Shkarupylo V., Alsayaydeh J.A.J, Tomičić I. et al. A technique for checking the adequacy of formal model // ARPN Journal of Engineering and Applied Sciences, 2021, Vol. 16, No 16, pp. 1707—1719. URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85118181893&origin=resultslist.
14. Шкарупило В.В., Чемерис О.А., Душеба В.В. та ін. Модельно-орієнтований підхід до контролю показників нефункціональних характеристик під час проєктування // Вчені записки Таврійського національного університету ім. В.І.Вернадського. Серія «Технічні науки», 2021, 32 (71), Ч. 1, № 1, с. 166—171. DOI: https://doi.org/10.32838/ 2663-5941/2021.1-1/27.
15. Shkarupylo V. A Technique of DEVS-Driven Validation. In Modern Problems of Radio Engineering, Telecommunications, and Computer Science: Р XIIIth Int. Conf., TCSET'2016 (Lviv-Slavske, Ukraine, February 23-26, 2016), рр. 495—497. DOI: 10.1109/TCSET.2016.7452097.
16. Van Tendeloo Y., Vangheluwe H. An evaluation of DEVS simulation tools // Simulation, 2017, Vol. 93, No 2, pp. 103—121. DOI: https://doi.org/10.1177/0037549716678330.
17. Van Tendeloo Y., Vangheluwe H. Discrete event system specification modeling and simulation. Proceedings of the 2018 Winter Simulation Conference (Gothenburg, Sweden, 9-12 Dec. 2018), pp. 162—176. DOI: https://doi.org/10.1109/WSC.2018.8632372.
18. Шкарупило В.В., Кудерметов Р.К., Польська О.В. DEVS-орієнтована методика валі­дації композитних веб-сервісів // Радіоелектроніка, інформатика, управління, 2015, № 4, c. 79—86. DOI: 10.15588/1607-3274-2015-4-12.
19. Shkarupylo V. A Simulation-driven Approach for Composite Web Services Validation. Proc. 27th Int. Central European Conference on Information and Intelligent Systems, CECIIS 2016 (Varazdin, Croatia, September 21-23, 2016). pp. 227—231. URL: http://archive. foi.hr/app/public/conferences/1/ceciis2016/papers/QoS-1.pdf
20. Tudose C. JUnit in Action: Third Edition. NY: Manning Publications Co, 2020, 560 p. ISBN 9781617297045.
21. Falcone Y., Krstić S., Reger G., Traytel D. A taxonomy for classifying runtime verification tools // International Journal on Software Tools for Technology Transfer, 2021, Vol. 23, pp. 255—284. DOI: https://doi.org/10.1007/s10009-021-00609-z.
22. Cohen E. et al. VCC: A Practical System for Verifying Concurrent C / eds. S. Berghofer, T. Nipkow, C. Urban, M. Wenzel. Theorem Proving in Higher Order Logics. TPHOLs 2009 // Lecture Notes in Computer Science, 2009, Vol. 5674. Berlin, Heidelberg: Springer, pp. 23—42. DOI: https://doi.org/10.1007/978-3-642-03359-9_2.
23. Nardone V., Santone A., Tipaldi M. et al. Model checking techniques applied to satellite operational mode management // IEEE Systems Journal, 2019, Vol. 13, No. 1, pp. 1018—1029. DOI: https://doi.org/10.1109/JSYST.2018.2793665.
24. Jenihhin M., Lai X., Ghasempouri T., Raik J. Towards multidimensional verification: where functional meets non-functional. NORCHIP and International Symposium of System-on-Chip (SoC): 2018 IEEE Nordic Circuits and Systems Conference (Tallinn, Estonia, 30-31 Oct. 2018), pp. 1—7. URL: https://arxiv.org/ftp/arxiv/papers/1908/1908. pdf.
25. Larman C. Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and Iterative Development. 3rd Edition. Pearson, 2004, 736 p. URL: https:// www.amazon.com/Applying-UML-Patterns-Introduction-Object-Oriented/dp/0131489062
26. Blinov I., Tankevych S. The harmonized role model of electricity market in Ukraine. 2016 2nd International Conference on Intelligent Energy and Power Systems. DOI: https:// org/ 10.1109/IEPS.2016.7521861
27. Lamport L. The PlusCal algorithm language // Theoretical Aspects of Computing: 6th Int. Colloquium, part of LNCS (Kuala Lumpur, Malaysia), 2009, Vol. 5684, pp. 36—60. URL: https://lamport.azurewebsites.net/pubs/pluscal.pdf.
28. Шкарупило В.В., Блінов І.В. Модельно-орієнтований підхід до формалізації нефункціональних характеристик систем критичного призначення, зокрема у природокористуванні. Глобальні та регіональні проблеми інформатизації в суспільстві і природокористуванні 2021. IX Міжнародна науково-практична Інтернет-конференція. Київ, Україна, 13-14 травня, 2021. Київ: НУБіП України, c. 55—57.
29. Шкарупило В.В., Чемерис О.А., Душеба В.В. та ін. Метод синтезу формальних специфікацій на основі трійок Хоара // Наукові праці ДонНТУ. Серія «Інформатика, кібернетика та обчислювальна техніка», 2020, № 1(30), с. 49—57. URL: https://iktv. donntu.edu.ua/wp-content/uploads/2021/01/07_Shkarupylo.pdf.
30. Clarke E.M., Grumberg O., Kroening D. et al. Model checking: 2nd ed. Massachusetts: The MIT Press, 2018. URL: https://mitpress.mit.edu/books/model-checking-second-edition.
31. Шкарупило В.В., Душеба В.В. Підхід до синтезу формалізованих подань нефункціональних характеристик на етапі проєктування. Безпека енергетики в епоху цифрової трансформації. ІІІ науково-практична конференція Інституту проблем моделювання в енергетиці ім. Г.Є. Пухова НАНУ, 22 грудня 2021 р. Київ : ІПМЕ ім. Г.Є.Пухова НАН України, 2021, с. 128—130.
32. Shkarupylo V.V., Blinov I.V., Chemeris A.A. et al. On Applicability of Model Checking Technique in Power Systems and Electric Power Industry / Zaporozhets A. (eds). Systems, Decision and Control in Energy III // Studies in Systems, Decision and Control, 2022, Vol. 399. DOI: https://doi.org/10.1007/978-3-030-87675-3_1.
33. Mesarovic M.D., Macko D., Takahara Y. Theory of hierarchical, multilevel, systems. New York: Academic Press, 1970, 294 p.
34. Блінов І.В. Проблеми функціонування та розвитку ринку електричної енергії України. (за матеріалами наукової доповіді на засіданні Президії НАН України 3 лютого 2021 р.) // Вісник НАН України, № 3, c. 20—28. DOI: https://doi.org/10.15407/publishing2019.54.005
35. Блінов І.В., Парус Є.В., Шкарупило В.В. Структура та моделі інформаційної взаємодії учасників ринку електричної енергії. Вінниця: ГО «Європейська наукова платформа», 2021, 114 с.

Повний текст: PDF