Об одном подходе к верификации симметрических параметризованных распределенных систем.

Авторы

Захаров В.А., Коннов И.В.

Аннотация

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

Один из способов решения указанной задачи заключается в поиске инварианта параметризованной системы. Инвариант представляет собой конечный процесс, способный заменить собой почти все системы бесконечного семейства. Автоматический поиск инварианта осуществляется путем проверки отношения симуляции между отдельными системами бесконечного семейства. В связи с этим большое значение придается выбору подходящего отношения симуляции. В статье предложено новое отношение симуляции - блочной симуляции. Для указанного отношения симуляции доказана монотонность операции синхронной композиции, а также монотонность отношения выполнимости формул одного широко известного класса $ACTL^*_{-X}$ темпоральной логики вычислительных деревьев. Предложенный метод опробован на нескольких примерах, включая ряд известных тестовых задач (например, задачу об обедающих философах, алгоритм взаимного исключения и др.), а также для более сложных синхронных систем (алгоритм распределения ресурсов кольце синхронных процессов). Результаты эксперимента подтвердили практичность и эффективность предложенного метода.

Издание

Программирование, 2005, № 5, с. 24-36.

Научная группа

Теоретическая информатика

Все публикации за 2005 год

Все публикации