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

В.В. Шкарупило 1, канд. техн. наук, В.В. Душеба 2, канд. техн. наук,
С.Ю. Скрупський 3, канд. техн. наук, І.В. Блінов 4, д-р техн. наук
1 Інститут проблем моделювання в енергетиці ім. Г.Є. Пухова НАН України
Україна, 03164, Київ, вул. Генерала Наумова, 15
Національний університет біоресурсів і природокористування України,
Україна, 03041, м. Київ, вул. Героїв Oборони, 15
тел.: +38 (066) 1297345; e-mail: Ця електронна адреса захищена від спам-ботів. Вам необхідно увімкнути JavaScript, щоб побачити її.;
2 Інститут проблем моделювання в енергетиці ім. Г.Є. Пухова НАН України
тел.: +38 (050) 4133988; e-mail: Ця електронна адреса захищена від спам-ботів. Вам необхідно увімкнути JavaScript, щоб побачити її.;
3 Національний Університет «Запорізька політехніка» МОН України
Україна, 69063, м. Запоріжжя, вул. Жуковського, 64
тел.: +38 (061) 7698249; e-mail: Ця електронна адреса захищена від спам-ботів. Вам необхідно увімкнути JavaScript, щоб побачити її.;
4 Інститут електродинаміки НАН України
Україна, 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 с.

ШКАРУПИЛО Вадим Вікторович, канд. техн. наук, доцент, ст. наук. cпівробітник від­ділу математичного та комп’ютерного моделювання Інституту проблем моделювання в енергетиці ім. Г.Є. Пухова НАН України, доцент кафедри комп’ютерних систем, мереж та кібербезпеки Національного університет біоресурсів і природокористування України. У 2010 р. закінчив Запорізький національний технічний університет. Область наукових досліджень — формальна верифікація, валідація, системи критичного призначення, кіберфізичні системи, Інтернет речей, веб-сервіси.

ДУШЕБА Валентина Віталіївна, канд. техн. наук, доцент, зав. відділу математичного та комп’ютерного моделювання Інституту проблем моделювання в енергетиці ім. Г.Є. Пу­хова НАН України. У 1984 р. закінчила Київський інститут інженерів цивільної авіації. Область наукових досліджень — високопродуктивні архітектури та обчислення.

СКРУПСЬКИЙ Степан Юрійович, канд. техн. наук, доцент, доцент кафедри комп’ю­терних систем та мереж Національного університету «Запорізька політехніка». У 2010 р. закінчив Запорізький національний технічний університет. Область наукових досліджень — розподілені системи, високопродуктивні обчислення, нейронні мережі, опрацювання даних.

БЛІНОВ Ігор Вікторович, д-р техн. наук, ст. наук. cпівробітник, заст. директора з наукової роботи Інституту електродинаміки НАН України. У 2005 р. закінчив Донець­кий національний технічний університет. Область наукових досліджень — моделюван­ня процесів ціноутворення на ринку електричної енергії з урахуванням мережевих та системних обмежень, методи пошуку місць пошкоджень в електричних мережах, прог­нозування електричного навантаження.

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