Skip to main navigation menu Skip to main content Skip to site footer

Scientific monographs

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

DOI
https://doi.org/10.36074/smtzfvappskp-monograph.2021
Published
28.12.2021

Abstract

Проведено порівняльний аналіз методів та засобів формальної верифікації, застосовуваних у процесі розроблення систем критичного призначення, зокрема – на етапі проєктування названого процесу. За результатами проведеного аналізу запропоновано і викладено комплексний підхід, що полягає у здійсненні контролю показників і функціональних, і нефункціональних характеристик названих систем вже на етапі проєктування процесу розроблення. Розглянуто модель подання функціональних характеристик розроблюваної системи у формальній специфікації, відмінними рисами якої є оперування трійками Гоара (C.A.R. Hoare) і відповідними аксіомами. За рахунок цього було досягнуто зменшення кількості рядків коду результуючої специфікації. Викладено запропонований метод синтезу формальних специфікацій функціональних характеристик розроблюваної системи, що будується на вищезазначеній моделі. У якості вихідних даних розглянуто блок-схему алгоритму, діаграму дій. За рахунок залучення виразних засобів темпоральної логіки дій Леслі Лемпорта (Leslie Lamport), а також алгоритмічної мови PlusCal, розроблений метод забезпечує механізм співставлення елементів аналітичного подання формальної специфікації функціональних характеристик із елементами подання рівня реалізації. Це відповідає центральній концепції Бертрана Мейера (Bertrand Meyer) – з точки зору безшовності сполучення застосовуваних виразних засобів, конструкцій. У якості сценаріїв предметної області, що реалізуються завдяки функціонуванню системи критичного призначення, опрацьовано сценарії космічної галузі, сценарії взаємодії учасників ринку електричної енергії на основі рольових моделей. Розглянуто складові рольової моделі ідентифікації учасників ринку електричної енергії з використанням формалізованого підходу, сценарії взаємодії учасників ринку електричної енергії на основі рольових моделей.

Монографію призначено для аспірантів технічних напрямів, фахівців з аудиту та менеджменту в електроенергетиці, науковців та фахівців у галузі інформаційного обміну та функціонування ринків електричної енергії, розробників, діяльність яких пов’язана із проєктуванням програмно-алгоритмічного забезпечення комп’ютерних систем, зокрема систем критичного призначення, вбудованих систем.

⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯

Рекомендовано до друку Вченою радою Інституту проблем моделювання в енергетиці ім.Г.Є.Пухова НАН України (протокол No 16 від 25 листопада 2021 року), Вченою радою Інституту електродинаміки НАН України (протокол No 11 від 18 листопада 2021 року).

⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯

REVIEWERS:

Лахно Валерій Анатолійович - доктор технічних наук, професор, завідувач кафедри комп’ютерних систем, мереж та кібербезпеки Національного університету біоресурсів і природокористування України, Україна

Зайцев Євген Олександрович - доктор технічних наук, старший науковий співробітник, провідний науковий співробітник Інституту електродинаміки Національної академії наук України, Україна

⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯

ЗМІСТ:

СКОРОЧЕННЯ ТА УМОВНІ ПОЗНАКИ

ПЕРЕДМОВА

РОЗДІЛ 1. АНАЛІЗ МЕТОДІВ ТА ЗАСОБІВ КОНТРОЛЮ АРТЕФАКТІВ ПРОЦЕСУ ПРОєКТУВАННЯ
1.1 Обгрунтування актуальності контролю артефактів проєктування
1.2 Підходи, методи та засоби контролю
   1.2.1 Специфіка методів перевірки на моделі
   1.2.2 Сфери застосування методів перевірки на моделі
   1.2.3 Темпоральна логіка дій та відповідні засоби
   1.2.4 Засоби контролю нефункціональних характеристик
   1.2.5 Підходи до перевірки адекватності артефактів
   1.2.6 Прийняті рішення та їх структура

РОЗДІЛ 2. ВИКЛАДЕННЯ МОДЕЛІ ПОДАННЯ СПЕЦИФІКАЦІЙ
2.1 Постановка вирішуваної задачі
2.2 Викладення підходу до вирішення задачі
   2.2.1 Застосовувані концепти та припущення
   2.2.2 Формалізація архітектурної складової
2.3 Формалізація рівнів подання моделі
   2.3.1 Аналітичне подання функціональних характеристик
      2.3.1.1 Застосування засобів структури Кріпке
      2.3.1.2 Застосування засобів числення процесів
   2.3.2 Формалізація на рівні реалізації
      2.3.2.1 Формалізація подій
      2.3.2.2 Формалізація станів

РОЗДІЛ 3. ВИКЛАДЕННЯ МЕТОДУ СИНТЕЗУ СПЕЦИФІКАЦІЙ
3.1 Постановка вирішуваної задачі
3.2 Формулювання підходу до вирішення задачі
3.3 Кроки розробленого методу
3.4 Дослідження сценаріїв застосування методу
   3.4.1 Дослідження послідовного сценарію
   3.4.2 Дослідження сценарію із поданням паралелізму
3.5 Опрацювання рівня реалізації специфікації

РОЗДІЛ 4. РОЗРОБЛЕННЯ СЦЕНАРІЇВ ВЗАЄМОДІЇ УЧАСНИКІВ РИНКУ ЕЛЕКТРИЧНОЇ ЕНЕРГІЇ НА ОСНОВІ РОЛЬОВИХ МОДЕЛЕЙ
4.1 Використання рольових моделей для опису організації ринку електричної енергії згідно концепції Smart Grid
4.2 Побудова рольових моделей ідентифікації учасників ринку електричної енергії України відповідно до вимог ENTSO-E

ВИСНОВКИ

ЛІТЕРАТУРА

⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯

Year of publication: 2021
Language: Ukrainian
Authors: Shkarupylo V.V., Blinov I.V.

Translation: No
Translator: -

Type: Hardcover book
Number of pages: 104

Format: 148x210x10mm
ISBN: 978-617-8037-55-0
UDC: 621.311 :004.052.42

References

  1. Харченко В. С. Аналіз проблем IT-інженерії безпеки: проект TEMPUS-SAFEGUARD. Радіоелектронні і комп’ютерні системи. 2010. № 7 (48). С. 297-300.
  2. Конорев Б. М., Манжос Ю. С., Харченко В. С., Алексеев Ю. Г., Сергиенко В. В., Чертков Г. Н. Инвариантно-ориентированная оценка качества программного обеспечения космических систем / под ред. Б. М. Конорева, В. С. Харченко. Харьков : Государственный центр регулирования качества поставок и услуг, Национальный аэрокосмический университет им. Н. Е. Жуковского «ХАИ», 2009. 224 с.
  3. Омельчук Л. Л. Формальні методи специфікації програм: навч. посібник. К. : УкрІНТЕІ, 2010. 78 с.
  4. Микрин Е. А. Бортовые комплексы управления космических аппаратов: учебное пособие. Москва : МГТУ им. Н. Э. Баумана, 2014. 245 с.
  5. Петрик В. Л. Экспертиза программного обеспечения информационно-управляющих систем с использованием дескрипторного семантического пространства. Радіоелектронні і комп’ютерні системи. 2007. № 2 (21). С. 29-35.
  6. ДСТУ EN 61508-3:2019. Функційна безпечність електричних, електронних, програмованих електронних систем, пов’язаних із безпекою. Частина 3. Вимоги до програмного забезпечення (EN 61508-3:2010, IDT; IEC 61508-3:2010, IDT). [Чинний від 2019-09-01]. URL: https://budstandart.ua/normativdocument.html?id_ doc=84385&minregion=852. (Accessed: 10.04.2021).
  7. ISO 26262:2018. Road vehicles. Functional safety. Part 1: Vocabulary. [Published: December 2018]. URL: https://www.iso.org/standard/68383.html (Accessed: 05.10.2020).
  8. Про затвердження Вимог з ядерної та радіаційної безпеки до інформаційних та керуючих систем, важливих для безпеки атомних станцій: наказ Державної інспекції ядерного регулювання від 22.07.2015 № 140, із змінами, внесеними згідно з Наказом Державної інспекції ядерного регулювання № 508 від 25.11.2019. URL: https://zakon.rada.gov.ua/laws/term/34229 (дата звернення: 26.03.2020).
  9. Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems (CENELEC - EN 50128), by European Committee for Electrotechnical Standardization (CENELEC), June 2020. URL: https://standards.globalspec.com/std/14317747/EN%2050128 (дата зверн.: 12.04.2021).
  10. Youn W. K., Hong S. B., Oh K. R., Ahn O. S. Software certification of safety-critical avionic systems: DO-178C and its impacts. IEEE Aerospace and Electronic Systems Magazine. 2015. Vol. 30, No. 4. P. 4 – 13. DOI: https://doi.org/10.1109/MAES.2014. 140109
  11. Харченко В.С., Скляр В.В., Конорев Б.М., Алексеев Ю.Г., Чертков Г.Н., Засуха С.А., Семенов Л.П. Оценка и обеспечение качества программных средств / под ред. Б.М. Конорева, В.С. Харченко. Харьков : Государственный центр регулирования качества поставок и услуг, Национальный аэрокосмический университет им. Н.Е. Жуковского «ХАИ», 2007. 244 с.
  12. Летичевський О. О. Символьні методи у верифікації та тестуванні високонадійних систем. Радіоелектронні і комп’ютерні системи. 2016. № 5(79). С. 78-83. URL: http://nbuv.gov.ua/UJRN/recs_2016_5_14
  13. 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 / eds. M. Broy, D. Peled, G. Kalus. Amsterdam : IOS Press, 2013. Vol. 34. P. 1-48. DOI: https://doi.org/10.3233/978-1-61499-207-3-1
  14. Manna Z., Pnueli A. Temporal verification of reactive systems: safety. Springer-Verlag : Berlin, Heidelberg, 1995. 530 p.
  15. Sharvia S., Papadopoulos Y. Integrating model checking with HiP-HOPS in model-based safety analysis. Reliability engineering & system safety. 2015. Vol. 135. P. 64-80.
  16. Reinertsen D. G. The principles of product development flow: second generation lean product development : 1st ed. Redondo Beach, CA : Celeritas Publishing, 2009. 304 p.
  17. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.
  18. Clarke E.M., Grumberg O., Kroening D., Peled D., Veith H. Model checking: 2nd ed. Massachusetts: The MIT Press, 2018.
  19. Вельдер С. Э., Лукин М. А., Шалыто А. А., Яминов Б. Р. Верификация автоматных программ. СПб.: Наука, 2011. 244 с.
  20. 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). P. 146-152. DOI: https://doi.org/10.1109/ISSREW.2017.43
  21. Pakonen A., Tahvonen T., Hartikainen M., Pihlanko M. Practical applications of model checking in the Finnish nuclear industry. Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies : Proc. 10th International Topical Meeting (San Francisco, CA, USA, 11-15 June 2017). P. 1342-1352.
  22. Shkarupylo V. V., Tomičić I., Kasian K. M., Alsayaydeh J. A. J. An Approach to increase the Effectiveness of TLC Verification with Respect to the Concurrent Structure of TLA+ Specification. International Journal of Software Engineering and Computer Systems. 2018. Vol. 4, No. 1. P. 48-60. DOI: https://doi.org/10.15282/ijsecs.4.1.2018.4.0037
  23. Камкин А.С. Введение в формальные методы верификации программ : учебное пособие. Москва: МАКС Пресс, 2018. 272 с.
  24. ДСТУ ISO 9000:2015. Системи управління якістю. Основні положення та словник термінів. [Чинний від 01.07.2016]. Вид. офіц. Київ : ДП «УкрНДНЦ», 2016. 45 с.
  25. IEEE 1012-2016. IEEE Standard for system, software, and hardware verification and validation. [Approved: 28 September 2017]. URL: https://ieeexplore.ieee.org/document/8055462. (дата звернення: 23.07.2020).
  26. Leucker M., Schallhart C. A brief account of runtime verification. The journal of logic and algebraic programming. 2009. Vol. 78, No. 5. P. 293-303.
  27. Falcone Y., Havelund K., Reger G. A Tutorial on Runtime Verification. NATO Science for Peace and Security Series - D: Information and Communication Security. Vol. 34: Engineering Dependable Software Systems. IOS Press, 2013. P. 141-175. DOI: https://www.doi.org/10.3233/978-1-61499-207-3-141
  28. Marmsoler D., Petrovska A. Detecting architectural erosion using runtime verification. Interaction and Concurrency Experience : 12th international scientific meeting (Lyngby, Denmark, June 20-21, 2019). EPTCS 304, 2019. P. 97-114.
  29. Marmsoler D. Hierarchical Specification and Verification of Architectural Design Patterns. Fundamental Approaches to Software Engineering : 21st International Conference (Thessaloniki, Greece, April 14-20, 2018). Thessaloniki, 2018. P. 149-168. DOI: 10.1007/978-3-319-89363-1_9
  30. Garlan D., Allen R., Ockerbloom J. M. Architectural mismatch: why reuse is still so hard. IEEE Software. 2009. Vol. 26, No. 4. P. 66-69.
  31. Myers G. J. Software reliability: principles and practices. NY : Wiley, 1976. 360 p.
  32. Rozier K. Y. Linear Temporal Logic symbolic model checking. Computer Science Review. 2011. Vol. 5, No. 2. P. 163-203.
  33. Curcin V., Ghanem M. M., Guo Y. Analysing scientific workflows with Computational Tree Logic. Cluster Computing. 2009. Nol. 12, No. 4. P. 399-419. DOI: 10.1007/ s10586-009-0099-6
  34. Kwiatkowska M., Norman G., Parker D. PRISM 4.0: verification of probabilistic real-time systems. Computer Aided Verification : International Conference. Part of LNCS (Snowbird, UT, USA, 14-20 July 2011). 2011. Vol. 6806. P. 585-591.
  35. Kapus T. Using PRISM model checker as a validation tool for an analytical model of IEEE 802.15.4 networks. Simulation Modelling Practice and Theory. 2017. Vol. 77. P. 367-378. DOI: https://doi.org/10.1016/j.simpat.2017.08.002
  36. Dimitrova R., Fioriti L. M. F., Hermanns H., Majumdar R. Probabilistic CTL∗: The Deductive Way. Tools and Algorithms for the Construction and Analysis of Systems : 22nd International Conference. Part of LNCS (Eindhoven, The Netherlands, April 2-8, 2016). 2016. Vol. 9636. P. 280-296. DOI: https://doi.org/10.1007/978-3-662-49674-9_16
  37. Abraham E., Jansen N., Wimmer R., Katoen J.-P., Becker B. DTMC model checking by SCC reduction. Quantitative Evaluation of Systems : 2010 Seventh International Conference, IEEE (Williamsburg, VA, USA, 15-18 Sept. 2010). 2010. P. 37-46. DOI: https://doi.org/10.1109/QEST.2010.13
  38. Dehnert C., Junges S., Katoen J.-P., Volk M. A Storm is coming: a modern probabilistic model checker. Computer Aided Verification, CAV 2017 : 29th International Conference. Part of LNCS (Heidelberg, Germany, July 24-28, 2017). 2017. Vol. 10427, Part II. P. 592-600.
  39. Fabarisov T., Yusupova N., Ding K., Morozov A., Janschek K. The efficiency comparison of the prism and storm probabilistic model checkers for error propagation analysis tasks. Industry 4.0. 2018. Vol. 3, No. 5. P. 229-231.
  40. Agha G., Palmskog K. A survey of statistical model checking. ACM Transactions on Modeling and Computer Simulation. 2018. Vol. 28, No. 1. P. 1-39. DOI: https://doi.org/10.1145/3158668
  41. Kraibi K., Ben Ayed R., Rehm J., Collart-Dutilleul S., Bon P., Petit D. Event-B Decomposition Analysis for Systems Behavior Modeling. Software Technologies (ICSOFT 2019) : 14th International Conference (Prague, Czech Republic, July 26-28, 2019). Vol. 1. P. 278-286. DOI: https://doi.org/10.5220/0007929602780286
  42. Butler M., Körner P., Krings S., Lecomte T., Leuschel M., Mejia L.-F., Voisin L. The first twenty-five years of industrial use of the B-method. Formal Methods for Industrial Critical Systems, FMICS 2020 : 25th Int. Conf. / eds. M. ter Beek, D. Ničković (Vienna, Austria, September 2-3, 2020). 2020. Lecture Notes in Computer Science, Vol.12327. Springer, Cham. P. 189-209. DOI: https://doi.org/10.1007/978-3-030-58298-2_8
  43. Biere A., Cimatti A., Clarke E.M., Strichman O., Zhu Y. Bounded model checking. Advances in computers. 2003. Vol. 58, No. 11. P. 117-148.
  44. Albarghouthi A., Dillig I., Gurfinkel A. Maximal specification synthesis. ACM SIGPLAN Notices. 2016. Vol. 51, No. 1. P. 789-801. DOI: https://doi.org/10.1145/2914770. 2837628
  45. Deng X., Dwyer M.B., Hatcliff J., Mizuno M. Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. Software Engineering, ICSE '02 : 24th International Conference (Orlando, Florida, May, 2002). 2002. New York, NY, United States : Association for Computing Machinery. P. 442-452. DOI: https://doi.org/10.1145/581339.581394
  46. Cook S.A. The complexity of theorem-proving procedures. Theory of computing, STOC '71 : Proceedings of the third annual ACM symposium, May 1971. P. 151-158. DOI: https://doi.org/10.1145/800157.805047
  47. Prasad M., Biere A., Gupta A. A survey of recent advances in SAT-based formal verification. International Journal on Software Tools for Technology Transfer. 2005. Vol. 7. P. 156-173. DOI: https://doi.org/10.1007/s10009-004-0183-4
  48. Bjorner N. Z3 and SMT in industrial R&D. Formal Methods, FM 2018, as Part of the Federated Logic Conference, FloC 2018 : 22nd International Symposium (Oxford, UK, July 15-17, 2018). Part of LNCS. Vol. 10951. Springer, Cham. P. 675-678. DOI: https://doi.org/10.1007/978-3-319-95582-7_44
  49. Hoare C. A. R. Communicating sequential processes. Communications of the ACM. 1978. Vol. 21, No. 8. P. 666-677.
  50. Gurov D., Lidström C., Nyberg M., Westman J. Deductive functional verification of safety-critical embedded c-code: an experience report / Eds. L. Petrucci, C. Seceleanu, A. Cavalcanti. Critical Systems: Formal Methods and Automated Verification. AVoCS 2017, FMICS 2017. Lecture Notes in Computer Science. Vol. 10471. Springer, Cham. DOI: https://doi.org/10.1007/978-3-319-67113-0_1
  51. Рудаков И.В., Гурин Р.Е. Разработка и исследование синтетического метода верификации программы с помощью SMT-решателей. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4. C. 49-64. DOI: 10.18698/ 0236-3933-2016-4-49-64
  52. Biere A., Cimatti A., Clarke E. M., Fujita M., Zhu Y. Symbolic model checking using SAT procedures instead of BDDs. Design Automation Conference, DAC '99 : 36th annual ACM/IEEE Conference (New Orleans, Louisiana, USA, June, 1999). 1999. P. 317-320. DOI: https://doi.org/10.1145/309847.309942
  53. Alur R., Dill D. L. A theory of timed automata. Theoretical Computer Science. 1994. Vol. 126, No. 2. P. 183-235. DOI: https://doi.org/10.1016/0304-3975(94)90010-8
  54. Kim J. H., Larsen K. G., Nielsen B., Mikucionis M., Olsen P. Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools. Formal Methods for Industrial Critical Systems, FMICS'2015 : International Workshop. Part of LNCS (Oslo, Norway, June 22-23, 2015). 2015. Vol. 9128. P. 47-61.
  55. Shkarupylo V. V., Kudermetov R. K., Polska O. V. On the approaches to cyber-physical systems simulation. Advances in Cyber-Physical Systems (ACPS). 2018. Vol. 3, No. 1. P. 51-54.
  56. Shkarupylo V., Kudermetov R. On the aspects of cyber-physical systems modeling with UPPAAL. Simulation-2018 : Proc. 6th Int. conference, September 12-14, 2018. Kyiv: Pukhov Institute for Modelling in Energy Engineering, 2018. P. 267-269.
  57. Czerwiński W., S. Lasota, Lazić R. S., Leroux J., Mazowiecki F. The reachability problem for Petri nets is not elementary. STOC 2019: Proc. 51st Annual ACM SIGACT Symposium on Theory of Computing (Phoenix, AZ, USA June, 2019). New York, NY, United States: Association for Computing Machinery, 2019. P. 24-33. DOI: https://doi.org/10.1145/3313276.3316369
  58. Bonneland F., Dyhr J., Jensen P.G., Johannsen M., Srba J. Simplification of CTL formulae for efficient model checking of Petri Nets. Application and Theory of Petri Nets and Concurrency, PETRI NETS 2018 : 39th International Conference (Bratislava, Slovakia, June 24-29, 2018). 2018. Lecture Notes in Computer Science. Vol. 10877. Springer, Cham. P. 143-163. DOI: https://doi.org/10.1007/978-3-319-91268-4_8
  59. Корнеев Г. А., Парфенов В. Г., Шалыто А. А. Верификация автоматных программ. Компьютерные науки и технологии : тезисы докладов Международной научной конференции, посвященной памяти проф. А. М. Богомолова, Саратов : СГУ, 2007. С. 66-69.
  60. Hoare C. A. R. An axiomatic basis for computer programming. Communications of the ACM. 1969. Vol. 12, No. 10. P. 576-583.
  61. Stroud C. E., Wang L.-T., Chang Y.-W. Introduction. Electronic design automation / edited by L.-T. Wang, Y.-W. Chang, K.-T. Cheng. Morgan Kaufmann, 2009. P. 1-38.
  62. 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). P. 1-7.
  63. Lang J., Prasetya I.S.W.B. Model checking a C++ software framework: a case study. Foundations of Software Engineering : 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium (Tallinn, Estonia, August 26-30, 2019). P. 1026-1036. DOI: 10.1145/3338906.3340453
  64. ADAPRO: A general-purpose application framework for multi-threaded applications with support for a configuration file and remote control. Written in C++14. URL: https://gitlab.cern.ch/adapos/adapro (дата звернення: 16.10.2019).
  65. Su J., Chen W.-H. Model based fault diagnosis system verification using reachability analysis. IEEE Transactions on Systems, Man, and Cybernetics: Systems. 2017. Vol. 49, No. 4. P. 742-751.
  66. Kokologiannakis M., Sagonas K. Stateless model checking of the Linux kernel’s read-copy update (RCU). International journal on software tools for technology transfer. 2019. Vol. 21, No. 3. P. 287-306.
  67. Musuvathi M., Qadeer S. Fair stateless model checking. ACM SIGPLAN Notices. 2008. Vol. 43, No. 6. P. 362-371.
  68. Kokologiannakis M., Lahav O., Sagonas K., Vafeiadis V. Effective stateless model checking for C/C++ concurrency. Proceedings of the ACM on Programming Languages. Dec. 2017. Vol. 2. P. 1-32. DOI: https://doi.org/10.1145/3158105
  69. Aichernig B. K., Tappler M. Probabilistic black-box reachability checking (extended version). Formal Methods in System Design. 2019. In press. P. 1-33.
  70. Yang Y., Zu Q., Ke W., Zhang M., Li X. Real-time system modeling and verification through labeled transition system analyzer. IEEE Access. 2019. Vol. 7. P. 26314-26323.
  71. Nardone V., Santone A., Tipaldi M., Liuzza D., Glielmo L. Model checking techniques applied to satellite operational mode management. IEEE Systems Journal. 2019. Vol. 13, No. 1. P. 1018-1029. DOI: https://doi.org/10.1109/JSYST.2018.2793665
  72. Milner R. A Calculus of Communicating Systems. Berlin Heidelberg : Springer-Verlag, 1980. 174 p. DOI: https://doi.org/10.1007/3-540-10235-3
  73. Омельчук Л. Л. Формальні методи специфікації програм: навч. посібник. К. : УкрІНТЕІ, 2010. 78 с.
  74. Katz G., Barrett C., Dill D. L., Julian K., Kochenderfer M. J. Reluplex: an efficient SMT solver for verifying deep neural networks. Computer aided verification, CAV 2017 : 29th International Conference (Heidelberg, Germany, July 24-28, 2017). Proceedings, Part I. P. 97-117.
  75. Шкарупило В. В., Євдокимов В. Ф., Душеба В. В. Застосування формальних методів для перевірки систем критичного призначення. Вчені записки Таврійського національного університету імені В.І.Вернадського, серія «Технічні науки». 2019. Том 30 (69), № 6. С. 188-193. DOI https://doi.org/10.32838/2663-5941/2019.6-1/34
  76. Шкарупило В. В., Євдокимов В. Ф., Душеба В. В. Аспекти застосування методів перевірки на моделі при проектуванні систем критичного призначення. Безпека енергетики в епоху цифрової трансформації, науково-практична конференція Інституту проблем моделювання в енергетиці ім. Г.Є. Пухова Національної академії наук України : програма та матеріали, 20 грудня 2019 р. Київ : ІПМЕ ім. Г.Є. Пухова НАН України, 2019. С. 94-96.
  77. Конорев Б. М., Сергієнко В. В., Туркін І. Б. Доказова незалежна верифікація та прогнозування прихованих дефектів критичного програмного забезпечення на базі диверсного вимірювання інваріантів. Інженерія програмного забезпечення. 2011. №1 (5). С. 5-15.
  78. ECSS-E-00A. Space engineering. Policy and principles. [Cancelled]. The Netherlands : ESA Publications Division, 1996. 46 p.
  79. ECSS-S-ST-00C – ECSS system. Description, implementation and general requirements. [Чинний від 2008-07-31]. AG Noordwijk, The Netherlands : ESA Requirements and Standards Division, 2008. 34 p. URL: https://ecss.nl/standard/ecss-s-st-00c-description-implementation-and-general-requirements-31-july-2008/ (дата звернення: 16.09.2019).
  80. Феррари Д. Оценка производительности вычислительных систем : пер. с англ. Горлина А. И. / под ред. В. В. Мартынюка. М. : Мир, 1981. 576 с.
  81. Shkarupylo V. V., Tomičić I., Kasian K. M. The investigation of TLC model checker properties. Journal of Information and Organizational Sciences. 2016. Vol. 40, No. 1. P. 145-152.
  82. Шкарупило В. Дослідження методу перевірки на моделі TLC. Глобальні та регіональні проблеми інформатизації в суспільстві і природокористуванні '2020 : VIII Міжнародна науково-практична Інтернет-конференція (м. Київ, Україна, 14-15 травня, 2020). 2020. Київ : НУБіП України. С. 84-86.
  83. Ларман К. Применение UML и шаблонов проектирования : 2-е изд. / пер с. англ. М : Издательский дом «Вильямс», 2004. 624 с.
  84. Lamport L. The PlusCal algorithm language. Theoretical Aspects of Computing : 6th Int. Colloquium, part of LNCS, (Kuala Lumpur, Malaysia, Aug. 2009). 2009. Vol. 5684. P. 36-60.
  85. Shkarupylo V., Kudermetov R., Timenko A., Polska O. On the Aspects of IoT Protocols Specification and Verification. Problems of Infocommunications. Science and Technology : 2019 International Scientific-Practical Conference (Kyiv, Ukraine, October 8-11, 2019). P. 93-96.
  86. Lamport L. Specifying systems: The TLA+ language and tools for hardware and software engineers. Boston : Addison-Wesley, 2002. 382 р.
  87. Lamport L. Specifying concurrent systems with TLA+. Calculational System Design: Marktoberdorf summer school materials / eds. M. Broy, R. Steinbroggen. Amsterdam : IOS Press, Jan. 2000. Vol. 173 of NATO Science Series, III: Computer and Systems Sciences. P. 183-247.
  88. Newcombe C. Why Amazon chose TLA+. Abstract State Machines, Alloy, B, TLA, VDM, and Z : ABZ 2014 Int. Conf., Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 2014. Vol. 8477. P. 25-39.
  89. Newcombe C., Rath T., Zhang F., Munteanu B., Brooker M., Deardeuff M. How Amazon web services uses formal methods. Communications of the ACM. 2015. Vol. 58, No. 4. P. 66-73. DOI: https://doi.org/10.1145/2699417
  90. Sputh B., Verhulst E., Mezhuyev V. OpenComRTOS: Formally developed RTOS for Heterogeneous Systems. 2010. DOI: http://doi.org/10.13140/2.1.1488.0006
  91. Verhulst E., Boute R. T., Faria J. M. S., Sputh B. H. C., Mezhuyev V. Formal Development of a Network-Centric RTOS: Software Engineering for Reliable Embedded Systems. Springer Publishing Company, Inc., 2011. 236 p.
  92. Taibi T., Herranz A., Moreno-Navarro J. J. Stepwise refinement validation of design patterns formalized in TLA+ using the TLC model checker. Journal of Object Technology. 2009. Vol. 8, No. 2. P. 137-161.
  93. Beers R. Pre-RTL formal verification: an Intel experience. Design Automation Conference, DAC '08: Proceedings of the 45th annual Conference (Anaheim, California, June 2008). New York, NY, United States : Association for Computing Machinery, 2008. P. 806-811. DOI: https://doi.org/10.1145/1391469.1391675
  94. Kuppe M. A., Lamport L., Ricketts D. The TLA+ Toolbox. Formal Integrated Development Environment, F-IDE 2019 : 5th Workshop (Porto, Portugal, October 7, 2019). EPTCS 310, 2019. P. 50-62. DOI: http://doi.org/10.4204/EPTCS.310.6
  95. Yin J.-Q., Zhu H.-B., Fei Y. Specification and verification of the Zab protocol with TLA+. Journal of Computer Science and Technology. 2020. Vol. 35, No. 6. P. 1312-1323. DOI: https://doi.org/10.1007/s11390-020-0538-7
  96. Shkarupylo V.V. On the applicability of model checking techniques in the Internet of Things domain. Тиждень науки-2018: науково-практ. конф., 16–20 квітня 2018 р.: тези доп. Запоріжжя: ЗНТУ, 2018. С. 967–968.
  97. Shkarupylo V., Polska O., Shcherbak N. On the classification of model checking methods for the Internet of Things. Сучасні проблеми і досягнення в галузі радіотехніки, телекомунікацій та інформаційних технологій: IX Міжнародна науково-практична конференція, 3-5 жовтня 2018 р.: тези доп. Запоріжжя: ЗНТУ, 2018. С. 77–78.
  98. Kim Y.-M., Kang M. Formal verification of SDN-based firewalls by using TLA+. IEEE Access. 2020. Vol. 8. P. 52100-52112. DOI: https://doi.org/10.1109/ACCESS.2020.2979894
  99. Lamport L. Checking a multithreaded algorithm with +CAL. Distributed Computing, DISC'06 : Proceedings of the 20th international conference (Stockholm, Sweden, September 18-20, 2006). P. 151-163. DOI: https://doi.org/10.1007/11864219_11
  100. Zeller P., Bieniusa A., Ferreira C. Teaching practical realistic verification of distributed algorithms in Erlang with TLA+. Erlang 2020: Proceedings of the 19th ACM SIGPLAN International Workshop on Erlang (August, 2020). New York: Association for Computing Machinery, 2020. P. 14-23. DOI: https://doi.org/10.1145/3406085.3409009
  101. Konnov I., Kukovec J., Tran T.-H. TLA+ model checking made symbolic. Proceedings of the ACM on Programming Languages. 2019. Vol. 3, No. OOPSLA. P. 1-30. DOI: https://doi.org/10.5281/zenodo.3370063
  102. Ge N., Jenn E., Breton N., Fonteneau Y. Integrated formal verification of safety-critical software. International Journal on Software Tools for Technology Transfer (STTT). 2018. Vol. 20, No. 4. P. 423-440. DOI: https://doi.org/10.1007/s10009-017-0475-0
  103. Nouri A., Bensalem S., Bozga M., Delahaye B., Jegourel C., Legay A. Statistical model checking QoS properties of systems with SBIP. International Journal on Software Tools for Technology Transfer (STTT). 2015. Vol. 17, No. 2. P. 171-185. DOI: https://doi.org/10.1007/s10009-014-0313-6
  104. Ghezzi C., Sharifloo A. M. Model-based verification of quantitative non-functional properties for software product lines. Information and Software Technology. 2013. Vol. 55, No. 3. P. 508-524. DOI: https://doi.org/10.1016/j.infsof.2012.07.017
  105. Singh P., Singh L. Verification of safety critical and control systems of nuclear power plants using Petri nets. Annals of Nuclear Energy. 2019. Vol. 132. P. 584-592. DOI: https://doi.org/10.1016/j.anucene.2019.06.027
  106. Huang L., Kang E.-Y. Formal verification of safety & security related timing constraints for a cooperative automotive system / Eds. R. Hähnle, W. van der Aalst. Fundamental Approaches to Software Engineering. FASE 2019. Lecture Notes in Computer Science. 2019. Vol. 11424. Springer, Cham. P. 210-227. DOI: https://doi.org/10.1007/978-3-030-16722-6_12
  107. Weissnegger R., Pistauer M., Kreiner C., Römer K., Steger C. A novel design method for automotive safety-critical systems based on UML/MARTE. Proceedings of the 2015 Forum on specification & Design Languages (Barcelona Spain, September 14–16, 2015). Belmont, France, 2015. P. 177-184.
  108. Weissnegger R., Schuss M., Kreiner C., Pistauer M., Römer K., Steger C. Simulation-based verification of automotive safety-critical systems based on EAST-ADL. Procedia Computer Science. 2016. Vol. 83. P. 245-252. DOI: https://doi.org/10.1016/j.procs. 2016.04.122.
  109. Correa T., Becker L. B., Farines J.-M., Bodeveix J.-P., Filali M., Vernadat F. Supporting the design of safety critical systems using AADL. Proc. 2010 15th IEEE International Conference on Engineering of Complex Computer Systems (Oxford, UK, March 22–26, 2010). P. 331-336. DOI: https://doi.org/10.1109/ICECCS.2010.56
  110. Van Tendeloo Y., Vangheluwe H. An evaluation of DEVS simulation tools, SIMULATION. 2017. Vol. 93, No. 2. P. 103-121. DOI: https://doi.org/10.1177/0037549716678330.
  111. 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.
  112. Shkarupylo V. A Technique of DEVS-Driven Validation. Proc. XIIIth Int. Conf. on Modern Problems of Radio Engineering, Telecommunications, and Computer Science, TCSET'2016 (Lviv-Slavske, Ukraine, February 23–26, 2016). P. 495-497. DOI: 10.1109/TCSET.2016.7452097
  113. Шкарупило В.В., Скрупский С.Ю., Кудерметов Р.К. DEVS-модель как средство валидации композитных веб-сервисов распределенной системы. Комп’ютерно-інтегровані технології: освіта, наука, виробництво. 2011. № 7. С. 61-67.
  114. Heimdahl M.P.E., George D., Weber R. Specification test coverage adequacy criteria = specification test generation inadequacy criteria. High Assurance Systems Engineering: Eighth IEEE International Symposium (Tampa, FL, USA, March 25-26, 2004). 2004. P. 178-186, DOI: https://doi.org/10.1109/HASE.2004.1281742
  115. Pakonen A., Buzhinsky I. Verification of fault tolerant safety I&C systems using model checking. Industrial Technology, ICIT 2019: 2019 IEEE International Conference (Melbourne, Australia, 2019). 2019. P. 969-974. DOI: https://doi.org/10.1109/ICIT. 2019.8755014.
  116. Gay G., Rajan A., Staats M., Whalen M., Heimdahl M.P.E. The effect of program and model structure on the effectiveness of MC/DC test adequacy coverage. ACM Transactions on Software Engineering and Methodology. 2016. Vol. 25, No. 3. P. 25:1-25:34. DOI: https://doi.org/10.1145/2934672
  117. Cohen E., Dahlweid M., Hillebrand M., Leinenbach D., Moskal M., Santen T., Schulte W. 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. P. 23-42. DOI: https://doi.org/10.1007/978-3-642-03359-9_2
  118. Naumchev A., Meyer B. Seamless requirements. Computer Languages, Systems & Structures. 2017. Vol. 49. P. 119-132. DOI: https://doi.org/10.1016/j.cl.2017.04.001.
  119. Шкарупило В.В., Блінов І.В., Душеба В.В., Тіменко А.В. Дуальний підхід до формалізації функціональних характеристик систем критичного призначення. European scientific discussions : 9th International scientific and practical conference. Potere della ragione Editore (м. Рим, Італія, 18-20 липня, 2021 р.). С. 143-149. URL: https://sci-conf.com.ua/wp-content/uploads/2021/07/EUROPEAN-SCIENTIFIC-DISCUSSIONS-18-20.07.2021.pdf
  120. Томашевський В.М. Моделювання систем. Київ : Видавнича група BHV, 2005. 352 с.
  121. Gupta H.V., Clark M.P., Vrugt J.A., Abramowitz G., Ye M. Towards a comprehensive assessment of model structural adequacy. Water Resources Research. 2012. Vol. 48, No. 8. P. 1-16. DOI: https://doi.org/10.1029/2011WR011044.
  122. Babai L. Graph isomorphism in quasipolynomial time. Theory of Computing, STOC '16: 48th annual ACM symposium (Cambridge, MA, USA, June 18-21, 2016). P. 684-697.
  123. Mesarovic M. D., Macko D., Takahara Y. Theory of hierarchical, multilevel, systems. New York : Academic Press, 1970. 294 p.
  124. Alsayaydeh J. A. J., Shkarupylo V., Hamid M. S. B., Skrupsky S., Oliinyk A. Stratified model of the Internet of Things infrastructure. Journal of Engineering and Applied Sciences. 2018. Vol. 13, No. 20. P. 8634-8638. DOI: http://dx.doi.org/10.3923/ jeasci.2018.8634.8638
  125. Shkarupylo V., Polska O. The Approach to SDN Network Topology Verification on a Basis of Temporal Logic of Actions. Proc. 14th Int. Conf. on Advanced Trends in Radioelectronics, Telecommunications and Computer Engineering, TCSET'2018 (Lviv-Slavske, Ukraine, February 20–24, 2018). P. 183–186. doi: https://doi.org/10.1109/ TCSET.2018.8336182
  126. Shkarupylo V. V., Timenko A. V. On the expediency of stratification to foster the reconfigurability of formal specifications. Тенденції та вектор розвитку науки в сучасному світі: VI Міжнародна науково-практична інтернет-конференція: тези доповідей, Дніпро, 30 квітня 2018 р. Ч. 1. Дніпро: НБК, 2018. С. 46–49.
  127. Shkarupylo V. , Kudermetov R., Golub T., Polska O., Tiahunova M. Towards Model Checking of the Internet of Things Solutions Interoperability. Problems of Infocommunications. Science and Technology: proc. 2018 IEEE International Scientific and Practical Conference (Kharkiv, Ukraine, October 9-12, 2018). P. 465-468. DOI: https://doi.org/10.1109/INFOCOMMST.2018.8632037
  128. Шкарупило В.В., Чемерис О.А., Душеба В.В., Кудерметов Р.К., Польська О.В. Метод синтезу формальних специфікацій на основі трійок Хоара. Наукові праці ДонНТУ, Серія “Інформатика, кібернетика та обчислювальна техніка”. 2020. № 1(30). С. 49-57. DOI: 10.31474/1996-1588-2020-1-30-49-57.
  129. Гуц А.К. Математическая логика и теория алгоритмов. Омск : Наследие. Диалог-Сибирь, 2003. 108 с.
  130. Шкарупило В.В. Про застосування правила композиції при синтезі формальних специфікацій. Науково-технічна конференція молодих вчених та спеціалістів Інституту проблем моделювання в енергетиці ім. Г.Є. Пухова НАН України, 15 травня 2020 р. Київ : ІПМЕ ім. Г.Є. Пухова НАН України, 2020. С. 20-21.
  131. Shkarupylo V., Chemerys O., Dusheba V., Kudermetov R., Oliinyk A. On Hoare triples applicability to dependable system specification synthesis. Dependable Systems, Services and Technologies, DESSERT'2020 : The 11th International Conference (Kyiv, Ukraine, May 14-18, 2020). P. 371-375. DOI: https://doi.org/10.1109/DESSERT50317.2020.9125074
  132. Кропачева М. С., Легалов А. И. Формальная верификация программ, написанных на функционально-потоковом языке параллельного программирования. Моделирование и анализ информационных систем. 2012. Т. 19, № 5. С. 81-99.
  133. Shkarupylo V. V., Timenko A. V. On the interoperability and consistency aspects with respect to the Internet of Things domain. Engineering sciences: development prospects in countries of Europe at the beginning of the third millennium: Collective monograph. Vol. 2. Riga : Izdevnieciba “Baltija Publishing”. 2018. P. 466-485.
  134. Timenko A.V., Shkarupylo V.V., Oliinyk A.O., Hrushko S.S. Formal Model for Checking the Interoperability Between the Components of the IoT system. Problemele Energeticii Regionale. 2019. Vol. 40, No. 1-1. P. 69-78. DOI: 10.5281/zenodo. 3239196.
  135. Dahl O.-J., Dijkstra E.W., Hoare C.A.R. Structured programming: 10th printing. London, UK : Academic Press Ltd., 1982. P. 1-82.
  136. Шкарупило В. В., Кудерметов Р. К., Польська О.В. DEVS-орієнтована методика валідації композитних веб-сервісів. Радіоелектроніка, інформатика, управління. 2015. № 4. С. 79-86. DOI: 10.15588/1607-3274-2015-4-12
  137. Про ринок електричної енергії: Закон України № 2019-VIII від 13.04.2017
  138. Блінов І.В. Проблеми функціонування та розвитку ринку електричної енергії України. (за матеріалами наукової доповіді на засіданні Президії НАН України 3 лютого 2021 р.). Вісник НАН України. 2021. № 3. С. 20-28. doi: https://doi.org/10. 15407/visn2021.03.020
  139. Блінов І.В. Теоретичні та практичні засади функціонування конкурентного ринку електроенергії. К.: Наукова думка, 2015. 250 с.
  140. Ivanov H., Blinov I., Parus Ye. Simulation Model of New Electricity Market in Ukraine// 2019 IEEE 6th International Conference on Energy Smart Systems (ESS). 2019. P. 339-342. DOI: https://doi.org/10.1109/ESS.2019.8764184
  141. Кириленко О.В., Блінов І.В., Парус Є.В., Іванов Г.А. Імітаційна модель ринку електричної енергії «на добу наперед» з неявним врахуванням мережевих обмежень енергетичних систем // Технічна електродинаміка. 2019. № 5. С. 60-67. DOI: https://doi.org/10.15407/techned2019.05.060
  142. Іванов Г.А., Блінов І.В., Парус Є.В. Комплексна розрахункова модель ринку на добу наперед та балансуючого ринку електроенергії України // Промелектро. 2016. № 4-5. С. 8–12.
  143. Блінов І.В., Парус Є.В., Іванов Г.А. Імітаційне моделювання функціонування балансуючого ринку електроенергії з урахуванням системних обмежень на параметри режиму ОЕС України // Технічна електродинаміка. 2017. №6. С. 72–79. DOI: https://doi.org/10.15407/techned2017.06.072
  144. Парус Є.В., Блінов І.В. Складові імітаційної моделі процесів ціноутворення на ринку електричної енергії України // Праці Інституту електродинаміки НАН України. імітаційна2019. Вип. 53. С. 28–34.
  145. Куцан Ю.Г., Блінов І.В., Іванов Г.А. Моделювання тарифо- та ціноутворення на роздрібному ринку електричної енергії України в нових умовах функціонування // Електронне моделювання. 2017. № 5. С. 71–79.
  146. Блінов І.В., Парус Є.В., Мірошник В.О., Шиманюк П.В. Сичова В.В. Модель оцінки доцільності переходу промислових споживачів до погодинного обліку електричної енергії на роздрібному ринку. Енергетика: економіка, технології, екологія». 2021. №1. С. 88-97. DOI: https://doi.org/10.20535/1813-5420.1.2021.242186
  147. Blinov I., Parus E. Approach of Reactive Power Pricing for Ancillary Service of Voltage Control in Ukraine. Intelligent Energy and Power Systems (IEPS), 2014 IEEE International Conference on. 2014. P. 145 – 148.
  148. Кириленко О.В., Блінов І.В., Парус Є.В. Оцінка роботи електростанцій при наданні допоміжних послуг з первинного та вторинного регулювання частоти в ОЕС України. Технічна електродинаміка. 2013. № 5. С. 55 – 60.
  149. Кириленко О.В., Блінов І.В., Парус Є.В., Трач І.В. Оцінка ефективності використання систем накопичення електроенергії в електричних мережах // Технічна електродинаміка. 2021. № 4. С 44-54. DOI:https://doi.org/10.15407/techned2021.04.044.
  150. Кириленко О.В., Блінов І.В., Парус Є.В. Оцінка роботи електростанцій при наданні допоміжних послуг з первинного та вторинного регулювання частоти в ОЕС України// Технічна електродинаміка. 2013. № 5. С 55-60.
  151. Блінов І.В., Парус Є.В. Спосіб реалізації аукціону пропускної спроможності міждержавних перетинів між ринками електричної енергії. Технічна електродинаміка. 2014. № 5. С. 56 – 58.
  152. Блінов І.В., О.Б. Рибіна, Є.В. Парус, С.Є. Танкевич. Математична модель розподілу пропускної спроможності міждержавних перетинів між двома ринками електричної енергії. Пр. Ін-ту електродинаміки НАН України. 2014. Вип. 37.С. 125-130.
  153. Блінов І.В., Парус Є.В. Врахування мережевих обмежень та мінімізація різниці цін між ринками електроенергії. Технічна електродинаміка. 2015. № 5. С. 8-88.
  154. Блінов І.В. Зональне ціноутворення як спосіб врахування мережевих обмежень на біржі електроенергії. Проблеми загальної енергетики. 2011. № 2(25). С. 49–53.
  155. Постанова Національної комісії, що здійснює державне регулювання у сферах енергетики та комунальних послуг №307 від 14.03.2018 «Про затвердження Правил ринку».
  156. Кириленко О.В., Денисюк С.П., Блинов И.В., и др. Интеллектуальные электроэнергетические системы: элементы и режимы. Под общ. ред. акад. НАН Украины А.В. Кириленко. К.: Ин-т электродинамики НАН Украины, 2014. 408 с.
  157. Інтелектуальні електричні мережі: елементи та режими. Під заг. Ред. Акад. НАН України Кириленко О.В.. К.: Ін-т електродинаміки НАН України, 2016. 400 с.
  158. Кириленко О.В. Блінов І.В., Корхмазов Г.С., Попович В.І. Інформаційно-технологічні системи конкурентного ринку електричної енергії в Україні. Проблеми загальної енергетики. 2009. № 19. С. 16–22.
  159. Блінов І.В., Кучанский В.В., Шкарупило В.В., Парус Є.В. Формалізація опису процесів організації взаємодії учасників та систем управління ринком електричної енергії на основі рольових моделей. The 12th International scientific and practical conference “World science: problems, prospects and innovations” (August 11-13, 2021) Perfect Publishing, Toronto, Canada. 2021. Р. 192-201.
  160. Шкарупило В.В., Блінов І.В., Душеба В.В., Тіменко А.В. Дуальний підхід до формалізації функціональних характеристик систем критичного призначення. The 9th International scientific and practical conference “European scientific discussions” (July 18-20, 2021) Potere della ragione Editore, Rome, Italy. 2021. Р. 143-149.
  161. Блінов І.В., Парус Є.В., Шкарупило В.В. Структура та моделі інформаційної взаємодії учасників ринку електричної енергії. 2021. Вінниця. «Європейська наукова платформа». С. 114.
  162. Блінов І. В., Жаркін А. Ф., Палачов С. О., Васильченко В. І. Впровадження сучасних стандартів для забезпечення функціонування системи управління генерацією згідно концепції Smart Grid // Innovations and prospects of world science. Proceedings of the 3rd International scientific and practical conference. Perfect Publishing. Vancouver, Canada. 2021. Pp. 21-27.
  163. Танкевич С.Є., Блінов І.В., Кириленко В.В. Україна та світ: нормативне забезпечення інтелектуальних електроенергетичних систем за концепцією Smart Grid. Стандартизація, сертифікація, якість. – 2014. – № 4 (89). – С. 38–44.
  164. ІEC/TR 63097:2017 Smart grid standardization roadmap. 2017. 315 p.
  165. Кириленко О.В., Блінов І.В., Танкевич С.Є. Smart Grid та організація інформаційного обміну в електроенергетичних системах. Технічна електродинаміка. 2012. № 3. С. 47–48.
  166. Іванов Г.А., Блінов І.В., Парус Є.В., Мірошник В.О. Складові моделі для аналізу впливу відновлювальних джерел енергії на ринкову вартість електроенергії в Україні// Технічна електродинаміка. 2020. № 4. C. 72-75. DOI: https://doi.org/10.15407/techned2020.04.072.
  167. Блінов І.В., Мірошник В.О., Шиманюк П.В. Короткостроковий інтервальний прогноз сумарного відпуску електроенергії виробниками з відновлювальних джерел енергії. Праці Інституту електродинаміки НАН України 2019. Вип. 54: С. 5-12. DOI: https://doi.org/10.15407/publishing2019.54.005.
  168. The conceptual model and its relation to market models for Smart Grids. SG-CG/M490/J_ General Market Model Development // CEN-CENELEC-ETSI Smart Grid Coordination Group. 2014. P.25
  169. The harmonised electricity market role model. Version: 2017-01 Approved. ENTSO-E AISBL. Brussels. 2017. P. 27.12.
  170. Кириленко О.В., Басок Б.І., Базєєв Є.Т., Блінов І.В. Енергетика України та реалії голобального потепління // Технічна електродинаміка. 2020. № 3. С 52-61.
  171. Блінов І.В., Парус Є.В. Вимоги до математичного забезпечення балансуючого ринку електричної енергії України. Технічна електродинаміка. 2012. № 2. С. 30–32.
  172. Blinov I., Kyrylenko O., Parus E., Rybina O. (2022) Decentralized Market Coupling with Taking Account Power Systems Transmission Network Constraints. Power Systems Research and Operation. Studies in Systems, Decision and Control, vol 388. Springer, Cham. DOI: https://doi.org/10.1007/978-3-030-82926-1_1
  173. Kuchanskyy V., Malakhatka D., Ihor B. Application of Reactive Power Compensation Devices for Increasing Efficiency of Bulk Electrical Power Systems. 2020 IEEE 7th International Conference on Energy Smart Systems (ESS), 2020, pp. 83-86. DOI: 10.1109/ESS50319.2020.9160072
  174. Blinov I., Zaitsev I.O., Kuchanskyy V.V. (2020) Problems, Methods and Means of Monitoring Power Losses in Overhead Transmission Lines. Systems, Decision and Control in Energy I. Studies in Systems, Decision and Control, vol 298. Springer, Cham. DOI: https://doi.org/10.1007/978-3-030-48583-2_8
  175. Blinov I., Trach I., Parus Y., Khomenko V., Kuchanskyy V., Shkarupylo V. Evaluation of The Efficiency of The Use of Electricity Storage Systems in The Balancing Group and The Small Distribution System. 2021 IEEE 2nd KhPI Week on Advanced Technology (KhPIWeek), 2021, pp. 262-265, DOI: 10.1109/KhPIWeek53812.2021.9569981
  176. Блінов І.В., Попович В.І. Гармонізована рольова модель європейського ринку електроенергії// Проблеми загальної енергетики. 2011. № 3(26). С. 5–11.
  177. Кириленко О.В., Блінов І.В., Корхмазов Г.С., Попович В.І. Рольова модель конкурентного оптового ринку електричної енергії в Україні: концептуальна схема, сегменти та ролі учасників. Пр. Ін-ту електродинаміки НАН України. Вип. 25. 2010. С. 5-13.
  178. Blinov, I., Tankevych, S. The harmonized role model of electricity market in Ukraine. In: 2016 2nd International Conference on Intelligent Energy and Power Systems, IEPS 2016 Conference Proceedings (2016). DOI: 10.1109/IEPS.2016.7521861
  179. Кириленко О.В., Блінов І.В., Попович В.І., Олефір Д.О. Методологія об’єктно-орієнтованого моделювання для опису функціонування конкурентного оптового ринку електричної енергії. Проблеми загальної енергетики. 2011. Вип. 1(24). С. 5–10.