Препринты Института систем информатики СО РАН 2013 г.

Стандартный язык диаграмм последовательных сообщений MSC применяется для описания сценариев взаимодействия объектов. В частности, он используется для спецификации поведения в системах реального времени и телекоммуникационных протоколах. В работе рассматриваются все конструкции MSC-диаграмм и их расширений в виде HMSC-диаграмм, за исключением концепций интерпретируемых данных и времени. Описаны алгоритмы трансляции конструкций MSC в раскрашенные сети Петри (CPN). Представлена программная система, реализующая эти алгоритмы. Приведены примеры трансляции, которые анализируются с помощью известной системы CPNTools.

В работе описан концептуальный базис улучшенного трехуровневого метода верификации C# программ. Язык C#-light расширен на небезопасный код. Определена формальная операционная семантика языков C#-light и C#-kernel на основе предметно-ориентированных систем переходов. Предложен подход к генерации условий корректности, базирующийся на логике безопасности языка C#-kernel. Новая концепция языка C#-kernel рассматривает его как объединения языка C#-light с выделенными элементами языка Atoment. Трансляция C#-light программы в C#-kernel сведена к преобразованию состояния программы на основе метода атрибутных аннотаций и предвычислению константных выражений языка C#.