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

Препринт 171

С.А. Черненок, В.А. Непомнящий

Анализ MSC-диаграмм распределенных систем с помощью раскрашенных сетей Петри

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

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

Препринт в формате PDF (Русский)

Препринт 170

И.С. Ануреев

Концептуальный базис трехуровневого метода верификации C# програм

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

Препринт в формате PDF (Русский)