Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року)

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

Повний опис

Збережено в:

Бібліографічні деталі
Дата:	2017
Автор:	Летичевський, О.А.
Формат:	Стаття
Мова:	Ukrainian
Опубліковано:	Видавничий дім "Академперіодика" НАН України 2017
Назва видання:	Вісник НАН України
Теми:	З кафедри Президії НАН України
Онлайн доступ:	http://dspace.nbuv.gov.ua/handle/123456789/114458
Теги:	Додати тег Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:	Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року) / О.А. Летичевський // Вісник Національної академії наук України. — 2017. — № 2. — С. 30-36. — укр.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine

id	irk-123456789-114458
record_format	dspace
spelling	irk-123456789-1144582017-03-09T03:02:16Z Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року) Летичевський, О.А. З кафедри Президії НАН України Доповідь присвячено важливій проблемі створення методів та алгоритмів побудови високонадійних систем математичного забезпечення для програмно-технічних комплексів, які використовуються в критичних з точки зору безпеки галузях, таких як аерокосмічна, медична, телекомунікаційна, в ядерній енергетиці, у виробництві сучасного озброєння тощо. Процес розроблення високонадійних систем оснований на принципі зменшення ризику або повного виключення неспрацьовування засобів безпеки в системі. 2017 Article Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року) / О.А. Летичевський // Вісник Національної академії наук України. — 2017. — № 2. — С. 30-36. — укр. 0372-6436 http://dspace.nbuv.gov.ua/handle/123456789/114458 uk Вісник НАН України Видавничий дім "Академперіодика" НАН України
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection	DSpace DC
language	Ukrainian
topic	З кафедри Президії НАН України З кафедри Президії НАН України
spellingShingle	З кафедри Президії НАН України З кафедри Президії НАН України Летичевський, О.А. Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року) Вісник НАН України
description	Доповідь присвячено важливій проблемі створення методів та алгоритмів побудови високонадійних систем математичного забезпечення для програмно-технічних комплексів, які використовуються в критичних з точки зору безпеки галузях, таких як аерокосмічна, медична, телекомунікаційна, в ядерній енергетиці, у виробництві сучасного озброєння тощо. Процес розроблення високонадійних систем оснований на принципі зменшення ризику або повного виключення неспрацьовування засобів безпеки в системі.
format	Article
author	Летичевський, О.А.
author_facet	Летичевський, О.А.
author_sort	Летичевський, О.А.
title	Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року)
title_short	Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року)
title_full	Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року)
title_fullStr	Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року)
title_full_unstemmed	Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року)
title_sort	високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні президії нан україни 7 грудня 2016 року)
publisher	Видавничий дім "Академперіодика" НАН України
publishDate	2017
topic_facet	З кафедри Президії НАН України
url	http://dspace.nbuv.gov.ua/handle/123456789/114458
citation_txt	Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року) / О.А. Летичевський // Вісник Національної академії наук України. — 2017. — № 2. — С. 30-36. — укр.
series	Вісник НАН України
work_keys_str_mv	AT letičevsʹkijoa visokonadíjnísistemimatematičnogozabezpečennâstenogramanaukovoídopovídínazasídanníprezidíínanukraíni7grudnâ2016roku
first_indexed	2025-07-08T07:31:32Z
last_indexed	2025-07-08T07:31:32Z
_version_	1837063097367396352
fulltext	30 ISSN 1027-3239. Visn. Nac. Acad. Nauk Ukr. 2017. (2) ВИСОКОНАДІЙНІ СИСТЕМИ МАТЕМАТИЧНОГО ЗАБЕЗПЕЧЕННЯ Стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року Доповідь присвячено важливій проблемі створення методів та алгоритмів побудови високонадійних систем математичного забезпечення для прог- рам но-технічних комплексів, які використовуються в критичних з точки зору безпеки галузях, таких як аерокосмічна, медична, телекомунікаційна, в ядерній енергетиці, у виробництві сучасного озброєння тощо. Процес роз- роблення високонадійних систем оснований на принципі зменшення ризику або повного виключення неспрацьовування засобів безпеки в системі. Шановні члени Президії! Шановні колеги! Нерідко виникає питання: чому українські програмісти так ви- соко цінуються в зарубіжних країнах? Відповідь, на мій погляд, полягає в традиціях виховання спеціалістів у нашій країні. З од- ного боку, на старших курсах університетів фахові дисципліни викладають зазвичай співробітники академічних інститутів, які ознайомлюють студентів з найбільш загальними сучасни- ми методами й технологіями комп’ютерної науки, що мають широке поле застосування. З іншого боку, на молодших курсах університетів студентам забезпечується можливість опанувати широкий спектр фундаментальних знань. Тому українським програмістам притаманна гнучкість мислення та готовність до адаптації у різних спеціальних предметних галузях. Одній із таких сучасних технологій, яка основана на алгебра- їчній теорії інформаційних взаємодій у багатоагентних розпо- ділених середовищах і називається інсерційним моделюванням, і присвячено мою сьогоднішню доповідь на засіданні Президії НАН України. Важливим застосуванням інсерційного моделю- вання є створення високонадійних систем математичного за- безпечення. Надійність програмних систем є зовнішня та внутрішня. Зо- внішня забезпечує захист від несанкціонованого втручання, внутрішня — відсутність помилок, надійність та коректність внутрішньої взаємодії програмних компонентів. Інші аспек- ЛЕТИЧЕВСЬКИЙ Олександр Адольфович — академік НАН України, завідувач відділу теорії цифрових автоматів Інституту кібернетики ім. В.М. Глушкова НАН України ISSN 1027-3239. Вісн. НАН України, 2017, № 2 31 З КАФЕДРИ ПРЕЗИДІЇ НАН УКРАЇНИ ти надійності комп’ютерних систем пов’язані з надійністю систем технічного забезпечення. В Інституті кібернетики ім. В.М. Глушкова НАН України та в інститутах Кібернетичного центру НАН України проводяться досліджен- ня, які охоплюють усі аспекти проблеми надій- ності програмних систем. Однак у цій доповіді ми обмежимося лише розглядом внутрішньої надійності. Вимоги високої надійності насамперед сто- суються систем, критичних до безпеки (так званих safety-critical systems). До таких систем, зокрема, належать системи, які використову- ють в аерокосмічній і медичній галузях, в ядер- ній енергетиці, виробництві сучасної зброї, управлінні залізницями, в автомобільній про- мисловості, телекомунікаційній і мікропроце- сорній індустрії та ін. Відмови в цих системах пов’язані із загрозою життю людей, втратою чи руйнуванням устаткування, забрудненням навколишнього середовища тощо. Процес роз- роблення високонадійних систем оснований на принципі зменшення ризику або повного виключення неспрацьовування умови безпеки в роботі системи. Програмна інженерія систем, критичних до безпеки, ґрунтується на включенні в процес розроблення процедур верифікації та валіда- ції. Сучасні методи верифікації потребують за- стосування формальних методів, побудови ма- тематичних моделей та генерації тестових на- борів, що забезпечують максимальне покриття програмних кодів. Проектування та аналіз складних систем на всіх етапах їх розроблення потребує побудови формальних моделей різних рівнів абстракції. Застосування формальних моделей дає змогу виявляти неправильні рішення, помилки та некоректності ще на ранніх етапах, що значно зменшує зусилля та заощаджує кошти порів- няно з тим випадком, коли ці помилки вияв- ляються на пізніх етапах розроблення або в готовій продукції. На рис. 1 наведено (щоправда, дуже спро- щено) фрагмент життєвого циклу системи математичного забезпечення та його транс- формацію в разі застосування технології ін- серційного моделювання. Основною особли- вістю цієї технології є побудова формальної моделі вимог на етапі дизайну та включення Рис. 1. Фрагмент життєвого циклу системи математичного забезпечення 32 ISSN 1027-3239. Visn. Nac. Acad. Nauk Ukr. 2017. (2) З КАФЕДРИ ПРЕЗИДІЇ НАН УКРАЇНИ процедур верифікації. Формальна модель ви- користовується також для генерації тестів, які забезпечують необхідні параметри надійності системи. На рис. 2 показано більш детальну схему розроблення високонадійних програмних сис- тем. Наведено етапи, на яких створюються та застосовуються формальні моделі системи. В інсерційних моделях систему представле- но у вигляді композиції середовища та агентів, занурених у нього. Середовище та агенти пред- ставлено як транзиційні (динамічні) системи, що еволюціонують у часі та мають спостережу- вану ззовні поведінку. Основи інсерційного моделювання було за- кладено наприкінці 90-х років минулого сто- ліття в роботах про модель взаємодії агентів та середовищ, а практичне використання ін- серційного моделювання відноситься до по- чатку 2000-х років, коли на замовлення фірми Motorola в українській компанії ISS (Informa- tion Software Systems) за участю співробітни- ків Інституту кібернетики ім. В.М. Глушкова НАН України було розроблено першу систему автоматичної верифікації вимог до програм- них систем VRS (верифікація вимог та специ- фікацій). В подальшому цю систему придбала американська компанія UniqueSoft, з якою ми й дотепер дуже плідно співпрацюємо. На осно- ві системи верифікації було створено нові за- соби проектування та дизайну, зокрема засоби тестування і генерації коду. Отже, математичною основою інсерційного моделювання є, як я вже говорив, алгебраїчна теорія взаємодії. Інсерційне моделювання уза- гальнює традиційні підходи до теорії взаємо- дії інформаційних процесів, основані на алге- брах та численнях процесів (CCS, CSP, ACP, π-числення, мобільні амбієнти та багато інших напрямів у загальній алгебро-логічній теорії Рис. 2. Загальна схема розроблення високонадійної системи модельним методом (із застосуванням інсерційних моделей) ISSN 1027-3239. Вісн. НАН України, 2017, № 2 33 З КАФЕДРИ ПРЕЗИДІЇ НАН УКРАЇНИ взаємодії). Основні методи, теоретичні та прак- тичні побудови в інсерційному моделюванні продовжують традиції школи В.М. Глушкова в комп’ютерній науці, що ґрунтуються на теорії автоматів, алгебрі алгоритмів, методах автома- тичної перевірки суджень, макроконвеєрних обчисленнях та ін. Базові принципи парадигми інсерційного моделювання, які мотивують його можливі за- стосування, прості й достатньо зрозумілі. Вони містять у собі такі положення (рис. 3). 1. Система складається з ієрархії середовищ та агентів, занурених у ці середовища. Мова може йти про технічні, програмно-технічні, а також про біологічні, соціальні та економічні системи. При побудові моделей таких систем нас цікавить передусім їх взаємодія в багато- агентному середовищі. 2. Середовища та агенти є об’єктами, що еволюціонують у часі та мають спостережу- вану поведінку. До таких систем належать як неперервні класичні динамічні системи, так і дискретні системи (автомати, транзиційні сис- теми, моделі програм). Поведінка системи ха- рактеризує її зовнішні інваріанти і є основою взаємодії. 3. Занурення нового агента в середовище змінює поведінку цього середовища. Як при- клад можна навести комп’ютер, який є середо- вищем для агентів — програм. Першою програ- мою, яку на ньому встановлюють, є, звичайно, операційна система, яка перетворює вихідний комп’ютер на юнікс- або віндовз-комп’ютер і, відповідно, змінює середовище, а установка сервісних агентів-програм забезпечує ефектив- ну взаємодію з компонентами комп’ютерного середовища та користувачами. 4. Середовище як агент може бути зануре- не у середовище вищого рівня. Ця двоїстість (агент як середовище та як простий агент, який, у свою чергу, може бути занурений в інше сере до вище) дуже важлива для побудови необмеженої рекурсивної динамічної ієрархії компонент складної системи. 5. У багаторівневому середовищі агенти мо- жуть переходити з одного середовища в інше (динамічність структури). 6. Агенти та середовища можуть моделюва- ти інших агентів та середовища на різних рів- нях абстракції. Ця властивість відкриває мож- ливість побудови когнітивних архітектур для моделювання розумової діяльності людини, а також створення інтелектуальних програмних систем (інтелектуальних агентів). Одним з основних досягнень теорії інсерцій- ного моделювання є побудова нової алгебри поведінок та її застосування при розв’язуванні багатьох важливих задач проектування надій- них систем. На відміну від традиційної теорії взаємодії, основаної на звичайних алгебрах та численнях процесів, в інсерційному моделю- ванні використовується неперервна багатоос- новна алгебра. Занурення агента в середовище змінює поведінку середовища за допомогою неперервного оператора занурення, який роз- глядається як один з операторів алгебри по- ведінок. Можливість збагачення алгебри пове- дінок введенням нових неперервних функцій та операторів дозволяє налаштовувати засоби проектування на необхідні проблемні області. Основним методом дослідження інсерцій- них моделей є символьне моделювання атри- бутних середовищ. Стани таких середовищ у символьному моделюванні є формулами чис- лення предикатів з кванторами, а програмні реалізації символьних моделей використову- ють системи автоматичної дедукції. Впровадження технології інсерційного мо- делювання здійснюється через компанію ISS, яка, як уже зазначалося, була заснована з до- помогою партнерів з компанії Motorola на по- чатку 2000-х років. Технологію було успішно Рис. 3. Схема базових принципів парадигми інсерцій- ного моделювання 34 ISSN 1027-3239. Visn. Nac. Acad. Nauk Ukr. 2017. (2) З КАФЕДРИ ПРЕЗИДІЇ НАН УКРАЇНИ апробовано в понад 150 проектах, виконаних спільно з фірмою Motorola у галузях мікро- процесорної, автомобільної, мережевої, теле- комунікаційної індустрії. Зараз в ISS працює вже понад 100 співробітників і виконуються замовлення зарубіжних компаній. Група, до складу якої входить близько 40 фахівців з Ін- ституту кібернетики ім. В.М. Глушкова НАН України та Національного технічного універ- ситету України «КПІ імені Ігоря Сiкорського», працює за сумісництвом у дочірній компанії IssSoft за технологією інсерційного моделю- вання та іншими передовими західними техно- логіями. Досвід, накопичений під час роботи із за- рубіжними компаніями, було використано для розроблення в Інституті кібернетики ім. В.М. Глушкова власної системи інсерцій- ного моделювання IMS (рис. 4), яка має за- соби для створення високонадійних систем математичного забезпечення. У розробленні цієї системи беруть активну участь співробіт- ники Херсонського державного університету. Засоби IMS включають програми символьної верифікації, генерації тестів із майже 100% покриттям коду або вимог, залежно від рівня абстракції моделі, програми генерації інваріан- тів, засоби оптимізуючих перетворень і рефак- торингу програм та їх моделей. Важливою сферою застосування цієї тех- нології є розпаралелювання обчислювальних процесів на багатопроцесорних обчислюваль- них машинах та організація ефективних об- числень у мережевих і хмарних системах. На- приклад, результати досліджень з інсерційного моделювання було використано при виконан- ні спільних проектів з фірмою Intel. Проведено дослідження з верифікації паралельних про- грам, створених у середовищі бібліотеки MPI, а також анотовано більшість бібліотечних функцій, достатніх для використання в про- цесі верифікації та експериментів з реальними проектами. У щойно завершеному проекті УНТЦ «Ког- нітивна архітектура для розуміння програмно- го забезпечення» було досліджено можливість Рис. 4. Верифікація та тестування в системі IMS ISSN 1027-3239. Вісн. НАН України, 2017, № 2 35 З КАФЕДРИ ПРЕЗИДІЇ НАН УКРАЇНИ автоматичної формалізації вимог, виражених природною мовою. Мова формальних моделей системи вклю- чає алгебро-логічні засоби опису поведінки си- стем у поєднанні із графічними мовами MSC та UCM, що належать до стандартів ITU. Фор- мальна семантика цієї мови представлена за допомогою інсерційних моделей. Ця семанти- ка використовується в процесі розроблення системи IMS, що забезпечує високу якість засобів. До складу системи IMS входять такі групи засобів. 1. Формалізація вимог. Засоби побудови ін- серційної моделі у вигляді атрибутного середо- вища та занурених у нього агентів (наприклад, телекомунікаційна система та користувачі). 2. Статична перевірка вимог. До цієї групи належать засоби перевірки властивостей сис- теми формалізованих вимог: • доведення повноти вимог (відсутність ту- пиків); • доведення несуперечливості (детермінізм вимог); • доведення властивостей безпеки. 3. Динамічна перевірка властивостей сис- теми, що задовольняє вимогам, генерація кон- кретних та символьних трас (сценаріїв функ- ціонування системи). Доведення динамічних властивостей виконується за допомогою роз- гортання системи рівнянь в алгебрі поведінок. Зокрема, цим забезпечується перевірка досяж- ності властивостей. 4. Дедуктивна система забезпечує перевір- ку властивостей, виражених у мові приклад- ного багатосортного (типізованого) числення предикатів першого ступеня, налаштованого на предметну галузь, до якої належить систе- ма. Дедуктивна система включає спеціалізо- вані прувери, алгоритми перевірки виконува- ності та розв’язування обмежень у змішаних чисельно-логічних теоріях та використовуєть- ся на всіх етапах проектування із застосуван- ням методу інсерційного моделювання. 5. Генерація та виконання тестів. Генерація тестів виконується на базі моделей вимог. Мо- делі системи, які з’являються на різних етапах розроблення, мають задовольняти вимогам, які лежать в основі проекту системи. Тому одним з основних критеріїв якості системи тестів є покриття всіх вимог до системи. Інші критерії залежать від рівня абстракції моделі. Для тес- тування готових кодів використовується, на- приклад, критерій покриття всіх рядків коду. Виконання тестів відбувається під керуванням моделі відповідного рівня абстракції. Досвід використання аналогічних засобів у компанії ISS здобуто в процесі верифікації та розроблення сотень систем із реального жит- тя та різних предметних галузей, у тому числі таких, як телекомунікації, вбудовані системи (зокрема, з автомобільної промисловості), сис- теми реального часу (наприклад, управління залізничною станцією) та ін. Об’єми інформації, які фігурують у вико- нуваних проектах, вимірюються такими пара- метрами: • десятки тисяч базових протоколів (фор- малізованих вимог); • сотні атрибутів; • сотні помилок, знайдених у документаціях; • тисячі тестів, що забезпечують повне по- криття вимог. Дослідження з теоретичних основ та мето- дів побудови систем, критичних до безпеки, із застосуванням формальних математичних методів проводяться в найбільших наукових центрах і компаніях Європейського Союзу та Сполучених Штатів Америки. Співпраця із зарубіжними IT-компаніями має великий по- зитивний вплив на молодих учених, які беруть участь у створенні промислових проектів, а потім застосовують набуті навички для розро- блення нових вітчизняних технологій. Сьогодні в Україні основи інсерційного мо- делювання викладаються в Київському наці- ональному університеті імені Тараса Шевчен- ка, Херсонському державному університеті та інших вищих навчальних закладах країни. До початку воєнних дій на Сході України курс ін- серційного моделювання читався також у До- нецькому національному університеті імені Василя Стуса. Таким чином в Україні посту- пово зростає кількість фахівців, які володіють 36 ISSN 1027-3239. Visn. Nac. Acad. Nauk Ukr. 2017. (2) З КАФЕДРИ ПРЕЗИДІЇ НАН УКРАЇНИ технологією інсерційного моделювання. За останні роки захищено 4 докторські та більш як 10 кандидатських дисертацій в галузі ство- рення високонадійних програмних систем. Отже, в Інституті кібернетики ім. В.М. Глуш- кова НАН України на базі технології інсерцій- ного моделювання та досвіду, накопиченого в процесі співробітництва із зарубіжними ком- паніями, розроблено вітчизняну технологію створення високонадійних програмних сис- тем, готову для впровадження в промислових організаціях. Проте широкому впровадженню у промисло- вих організаціях України сучасних методів по- будови високонадійних систем заважає відсут- ність належного фінансування. Ми докладаємо багато зусиль для пошуку міжнародної фінан- сової підтримки і сподіваємося отримати части- ну коштів, необхідних для продовження робіт з впровадження технології інсерційного моделю- вання, через систему міжнародних грантів, зо- крема за програмою «Горизонт-2020». За матеріалами засідання підготувала О.О. МЕЛЕЖИК

Високонадійні системи математичного забезпечення (стенограма наукової доповіді на засіданні Президії НАН України 7 грудня 2016 року)

Репозитарії

Схожі ресурси