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

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

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

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

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

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