Предложен метод построения формальных спецификаций с использованием MSC сценариев, а также алгоритм декомпозиции таких сценариев в атомарные переходы с целью последующей верификации. Подход позволяет верифицировать языки более высокого уровня, что упрощает процесс формализации, анализа, модификации и, как следствие, повышает качество формальной модели.
