Актуальний рівень розвитку програмної складової комп’ютерних систем, у тому числі розподілених, є таким, що потребує застосування комплексних підходів до організації процесу розроблення. Такі підходи включають, зокрема, кроки, спрямовані на залучення засобів формалізації, а також засобів автоматизації формалізованого опрацювання артефактів, що фігурують у процесі розроблення програмних систем, серед яких – і системи критичного призначення. Демонстративним свідченням дієвості такого підходу є, наприклад, виявлення у період від 2008 по 2020 рр. 66 підтверджених помилок у артефактах процесу розроблення систем керування, залучених для реалізації процесів, на основі яких уможливлюється функціонування атомної енергетики Фінляндії [1].
Доречно зауважити, однак, що корисний ефект від застосування формальних методів і засобів у процесі розроблення програмних систем, у тому числі розподілених, може проявлятися у різних формах:
– як підтвердження несуперечливості програмно-алгоритмічної складової розроблюваної системи, що особливо важливо у контексті розроблення систем критичного призначення, серед яких – і системи, на основі яких забезпечується реалізація процесів галузі енергетики [2];
– виявлення суперечливості програмно-алгоритмічної складової для обраного рівня деталізації досліджуваних артефактів як формалізованих подань. Аспект обрання належного рівня деталізації таких подань при цьому типово визначається рівнем кваліфікації, досвідом розробника / розробників. Відкритим, однак, і досі лишається питання розроблення і застосування теоретичних засад стосовно забезпечення автоматизації процесу встановлення достатнього рівня деталізації формалізованих подань, з урахуванням, у тому числі, доступних обчислювальних можливостей наявних комп’ютерних систем для їх залучення у якості програмно-апаратних платформ для проведення формальної верифікації зазначених артефактів в автоматизованому режимі.
Уваги заслуговує також і питання вибору технологій, на основі яких реалізуються розподілені програмні системи. Серед таких можуть бути, у тому числі, технології реалізації названих систем у формі вебсервісів: наприклад, згідно моделі централізованого координування відповідних компонентів. У даному контексті, результати попередніх досліджень дозволяють стверджувати стосовно дієвості залучення формальних методів та засобів для проведення валідації [3]. Результативність їх також було підтверджено у частині контролю сумісності компонентів розподілених програмних систем Інтернету речей [4].
Таким чином, формальні методи і супутні засоби є дієвими інструментами здійснення у процесі розроблення розподілених програмних систем контролю одержуваних при цьому артефактів, а також інструментами самоконтролю розробника / розробників. Питання автоматизації процесу вибору достатнього рівня деталізації формалізованих подань при цьому і досі є відкритим.
Подяки. Аналітичний матеріал висвітлено у відповідності до вирішуваних задач НДР 0120U102683 “Розроблення спеціалізованих комп’ютерних технологій моделювання та опрацювання оперативної інформації в задачах енергетики”, виконуваної відділом математичного та комп’ютерного моделювання Інституту проблем моделювання в енергетиці ім. Г.Є. Пухова НАН України.
Список літератури:
1. Pakonen A. Model-checking I&C logics – insights from over a decade of projects in Finland. Proc. 12th Nuclear Plant Instrumentation, Control and Human-Machine Interface Technologies, NPIC&HMIT 2021. American Nuclear Society (ANS), 2021. P. 792–801 DOI: https://doi.org/10.13182/T124-34322
2. Shkarupylo V., Blinov I., Dusheba V., Alsayaydeh J. A. J. Case Driven TLC Model Checker Analysis in Energy Scenario. Proc. of the Sixth International Workshop on Computer Modeling and Intelligent Systems, CMIS-2023 (Zaporizhzhia, Ukraine, May 3, 2023). P. 65–75. DOI: https://doi.org/10.32782/cmis/3392-6
3. 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. P. 227-231. URL: http://archive.ceciis.foi.hr/app/public/conferences/1/ceciis2016/papers/QoS-1.pdf
4. Timenko A.V., Shkarupylo V.V., Kulykovska N.A., Hrushko S.S. Study of the Method of Controlling the Compatibility of Internet of Things Devices Based on the MQTT Application Layer Protocol. Herald of Advanced Information Technology. Publ. Nauka i Tekhnika. Odessa: Ukraine. 2024, Vol. 7, No. 1, P. 48–58. DOI: https://doi.org/10.15276/hait.07.2024.4
|
Голосування 
Ця робота ліцензується відповідно до Creative Commons Attribution 4.0 International License
Знайшли помилку? Виділіть помилковий текст мишкою і натисніть Ctrl + Enter