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

Препринт 171
С.А. Черненок, В.А. Непомнящий
Анализ MSC-диаграмм распределенных систем с помощью раскрашенных сетей Петри

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

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

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

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




Вы обнаружили ошибку в следующем тексте:
Просто нажмите кнопку "Отправить сообщение об ошибке" для завершения. Вы можете также ввести комментарий (желательно).