Формальные методы анализа дискретных систем с использованием языка спецификаций - Крывый, С.Л.; Чугаенко, А.В. (Кибернетика и системный анализ, 2009)
Описано реалізацію алгоритму переведення набору діаграм MSC (документа MSC) в подійно еквівалентну йому мережу Петрі, наведено доказ коректності зазначеного алгоритму. Мережа, що отримана таким чином, може бути використана для аналізу властивостей вихідного документа MSC. Наведений алгоритм є складовою частиною системи аналізу та верифікації документів MSC.