Анотація до роботи:

Матвєєва Л.Є. Аналіз та верифікація MSC- систем за допомогою мереж Петрі. – Рукопис.

Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.03 – математичне та програмне забезпечення обчислювальних машин і систем. – Інститут кібернетики ім. В. М. Глушкова НАН України, Київ, 2005.

У дисертації розроблено автоматизований технологічний процес формальної специфікації та верифікації властивостей програмної (чи апаратної) системи, описаної інженерною мовою MSC’2000. Як математична модель використовуються мережі Петрі, які є адекватним механізмом описання властивостей дискретних реактивних систем, що включають асинхронні елементи та розподілені частини. За цією моделлю будується транзиційна система, на якій перевіряється виконуваність заданих специфікацій, що описують очікувану поведінку реальної системи. Перевірка моделі ґрунтується на розв’язанні систем лінійних однорідних і неоднорідних діофантових рівнянь над множиною натуральних чисел.

Загалом в роботі отримані такі результати: побудована низка алгоритмів, що разом складають єдиний автоматизований технологічний процес формальної специфікації та верифікації властивостей програмної (чи апаратної) системи, причому вхідною та вихідною мовами даного процесу є мова інженерного моделювання MSC’2000, доведена коректність алгоритмів, які входять до даного процесу. Зокрема, в роботі побудовано Алгоритм Перекладу з мови MSC’2000 у мережі Петрі, доведена коректність цього алгоритму за допомогою алгебри процесів; розроблені алгоритми верифікації наступних властивостей: (структурна) обмеженість, L3-живість, досяжність, наявність тупиків; розроблені та реалізовані оригінальні алгоритми побудови S- і T- інваріантів та пошуку пасток і тупиків асиметричних мереж Петрі; створена методика пошуку конфліктів функціональностей проектованої системи на основі поняття інваріантності властивостей базової моделі.

Робота всіх алгоритмів ілюструється відповідними експериментами, що демонструють коректність алгоритмів та всієї методики в цілому.

Головним результатом дисертації є побудова технологічної лінії, що дозволяє одночасно здійснювати процеси проектування та верифікації різних властивостей системи. Виконано завдання створення технологічного процесу аналізу й верифікації проектованої системи у вигляді набору діаграм мови MSC'2000 за допомогою мереж Петрі. Головні властивості даного технологічного процесу: по-перше, процес автоматизований, по-друге, вхідна мова і мова вихідних вердиктів є робочими мовам інженерів-розроблювачів. Технологічний процес – основа для побудови програмної системи перевірки моделі (model checker). При цьому отримані такі основні результати:

уперше побудовано Алгоритм Перекладу опису проектованої системи мовою MSC'2000 у мережу Петрі;

уперше розширена стандартизована формальна семантика мови MSC'2000 за рахунок доповнення її формальною семантикою елементу мови MSC'2000 <умова>;

доведено коректність Алгоритму Перекладу за допомогою алгебри процесів – бісімуляційна еквівалентність вхідних MSC діаграм та синтезованої за цими діаграмами мережі Петрі;

розроблений з реалізацією деяких фрагментів алгоритм для верифікації наступних властивостей формальної моделі: (структурна) обмеженість, L3-живість, досяжність, наявність дедлоків;

доведено коректність усіх кроків даного технологічного процесу;

у ході реалізації процесу були розроблені й реалізовані оригінальні алгоритми: побудови S- і T-інваріантів мережі Петрі та пошуку пасток і тупиків класу асиметричних мереж Петрі;

знижена обчислювальна складність задачі аналізу динамічних властивостей мережі Петрі, яка проводиться за допомогою розв’язання рівняння стану;

створено оригінальну методику пошуку конфліктів функціональностей проектованої системи за допомогою інваріантності властивостей базової формальної моделі.

Достовірність результатів дисертації випливає з логічності та строгості математичних доведень теорем та тверджень і підтверджена результатами експериментів.