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