Верификация параллельных и распределенных программных систем. Лекция 1

Доклад представляет новые результаты теоретической информатики в области верификации параллельных и распределенных программ. Верификация – это процесс проверки выполнения требований к поведению программной системы на всех возможных траекториях ее вычислений. Недавний революционный прорыв в области верификации связан с методом Model checking (проверка модели), который состоит в том, что истинность формулы темпоральной логики, описывающей требование к поведению программы, проверяется на модели программы.

Темпоральная логика – это модальная логика, позволяющая формализовать утверждения о поведении дискретных систем, истинность которых зависит от времени. В докладе рассматривается логика ветвящегося времени CTL* и ее подклассы – логики CTL и LTL. Темпоральные логики оказались удобным формализмом для задания свойств корректного поведения дискретных систем, взаимодействующих друг с другом и окружением. Истинность либо ложность формул этих логик определяется на структуре Крипке – одном из формализмов, описывающих реактивные (реагирующие) систем с конечным числом состояний. Структура Крипке К называется “моделью” темпоральной формулы Ф, если Ф истинна на К. В докладе рассматриваются алгоритмы Model checking, т.е. алгоритмы проверки выполнимости темпоральных формул на структурах Крипке.

Страница лекции на сайте Computer Science клуба