Научные направления:

3. ИНФОРМАТИКА (период 2003-2006 гг.) 3.3 Системы автоматизации, математические методы исследования сложных управляющих систем и процессов, CALS-технологии

Описание научного результата:

Предложен полиномиальный по сложности алгоритм нижней и верхней аппроксимаций проверки моделей для базовой логики действий с неподвижными точками — μ-исчисления. Изучена проблема проверки моделей для взаимодействующих распределенных агентов в терминах комбинированных логик знаний и действий с конструкциями для неподвижных точек. Реализован экспериментальный программный комплекс SPV (SDL Protocol Verifier), предназначенный для моделирования и верификации коммуникационных протоколов, включающий верификатор раскрашенных сетей Петри, который использует метод проверки моделей относительно свойств, представленных в μ-исчислении (рис. 1). Этот же метод реализован в системе верификации выполнимых спецификаций, представленных на языке Basic-REAL. Рис. 1. Схема верификации протокола.

http://www-sbras.nsc.ru/win/sbras/rep/rep2003/tom1/mat/math.html#5

[по направлениям] ||[по институтам] ||[по годам] ||[поиск] ||[содержание]