Главная страница « Научно-исследовательский семинар «

Заседание научно-исследовательского семинара. 11 июня 2008 г.

Доклад: «Верификация параметризованных моделей распределённых систем»
Докладчик: Коннов Игорь Владимирович, сотрудник лаборатории информационных систем факультета ВМК МГУ.

Предыдущее заседание « | 11.6.2008 | » Следующее заседание

Новости
Информация
Преподаватели и сотрудники
Студенты и аспиранты
Спецсеминары
Просеминар
Спецкурсы
Проекты
Ссылки
Поиск

В докладе рассматривается задача верификации моделей асинхронных распределённых систем, параметризованных по числу однотипных процессов. Задача актуальна в случае верификации моделей распределённых алгоритмов, сетевых протоколов и аппаратных схем, в которых число взаимодействующих процессов зависит от конфигурации системы. С помощью стандартных методов верификации моделей возможна проверка лишь конечного числа конфигураций параметризованной модели, в то время как в параметризованной модели число таких конфигураций бесконечно. В ходе исследования получены следующие результаты:

  1. Предложена новая модификация метода инвариантов, позволяющая сводить задачу верификации параметризованных систем асинхронно-взаимодействующих процессов к задаче верификации конечных моделей программ.

  2. На основе предложенного подхода разработаны новые алгоритмы верификации параметризованных систем асинхронно-взаимодействующих процессов, сочетающие методы верификации моделей программ (Model Checking) и проверки отношений симуляции между моделями программ.

  3. Практическая апробация предложенного метода и алгоритмов выполнена в виде экспериментальной системы, работоспособность которой продемонстрирована на нескольких примерах распределённых алгоритмов и сетевых протоколов.

Приглашаются аспиранты и стажеры программистских кафедр.

  

© Кафедра системного программирования ВМК МГУ.

Обновлено: 5.6.2008