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

У дисертації розроблено автоматизований технологічний процес формальної специфікації та верифікації властивостей програмної (чи апаратної) системи, описаної інженерною мовою MSC'2000. Як математична модель використовуються мережі Петрі. Перевірка моделі ґрунтується на використанні методів лінійної алгебри. Побудовано алгоритм перекладу опису проектованої системи мовою MSC'2000 у мережу Петрі, доведена коректність цього алгоритму за допомогою алгебри процесів. Розширена стандартизована формальна семантика мови MSC'2000 за рахунок доповнення її формальною семантикою елементу мови MSC'2000 <умова>. Розроблені алгоритми верифікації таких властивостей: (структурна) обмеженість, L3-живість, досяжність, відсутність тупиків. Розроблені та реалізовані оригінальні алгоритми побудови S- і T- інваріантів та пошуку пасток і тупиків асиметричних мереж Петрі. Створена методика пошуку конфліктів функціональностей проектованої системи на основі поняття інваріантності властивостей базової моделі.