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

Описана новая версия программного комплекса SRDSV2 (SDL/REAL Distributed Systems Verifier), предназначенного для моделирования, анализа и верификации распределенных систем, специфицированных на стандартном языке SDL. Этот комплекс включает транслятор из языка SDL в язык Dynamic-REAL (dREAL), систему автоматического моделирования dREAL-спецификаций и транслятор из языка dREAL в язык Promela, который является входным языком известной системы верификации методом проверки моделей SPIN. В этой версии программного комплекса SRDSV2 язык dREAL был расширен за счет введения процедур, что позволило уменьшить размер dREAL-спецификаций и их моделей в языке Promela. Описано применение этого комплекса для анализа и верификации динамической системы управления сетью касс-терминалов.

Эта работа частично поддержана грантом РФФИ № 11-07-90412-Ukr_f_a.

В данной работе представлен метод смешанной аксиоматической семантики, предлагаемый для верификации C-light программ. Данная семантика обладает однозначностью вывода (т. е. на каждом шаге допустимо одно и только одно правило вывода), а также имеет специальные варианты правил вывода для одной и той же программной конструкции, которые применяются в зависимости от типа переменной и дополнительной статической информации. Такой подход позволяет существенно упрощать условия корректности верифицируемых программ.

Работа частично поддержана грантом РФФИ № 11-01-00028.