Матвеева Л.Є. Аналіз та верифікація MSC- систем за допомогою мереж Петрі. - Рукопис. Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.03 - математичне та програмне забезпечення обчислювальних машин і систем. - Інститут кібернетики ім. В. М. Глушкова НАН України, Київ, 2005. У дисертації розроблено автоматизований технологічний процес формальної специфікації та верифікації властивостей програмної (чи апаратної) системи, описаної інженерною мовою MSC2000. Як математична модель використовуються мережі Петрі, які є адекватним механізмом описання властивостей дискретних реактивних систем, що включають асинхронні елементи та розподілені частини. За цією моделлю будується транзиційна система, на якій перевіряється виконуваність заданих специфікацій, що описують очікувану поведінку реальної системи. Перевірка моделі ґрунтується на розв'язанні систем лінійних однорідних і неоднорідних діафантових рівнянь над множиною натуральних чисел. Загалом в роботі отримані такі результати: побудована низка алгоритмів, що разом складають єдиний автоматизований технологічний процес формальної специфікації та верифікації властивостей програмної (чи апаратної) системи, причому вхідною та вихідною мовами даного процесу є мова інженерного моделювання MSC2000, доведена коректність алгоритмів, які входять до даного процесу. Зокрема, в роботі побудовано Алгоритм Перекладу з мови MSC2000 у мережі Петрі, доведена коректність цього алгоритму за допомогою алгебри процесів; розроблені алгоритми верифікації наступних властивостей: (структурна) обмеженість, LЗ-живість, досяжність, наявність тупиків; розроблені та реалізовані оригінальні алгоритми побудови S- і Т- інваріантів та пошуку пасток і тупиків асиметричних мереж Петрі; створена методика пошуку конфліктів функціональностей проектованої системи на основі поняття інваріантності властивостей базової моделі. Робота всіх алгоритмів ілюструється відповідними експериментами, що демонструють коректність алгоритмів та всієї методики в цілому. Ключові слова: MSC2000, автоматичний переклад, верифікація, мережі Петрі, алгебра процесів, семантика, формальні методи, система лінійних рівнянь, формальна специфікація.