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

Средства автоматической проверки темпоральных свойств асинхронных систем взаимодействующих процессовНИР

Соисполнители НИР

МГУ имени М.В.Ломоносова Координатор

Источник финансирования НИР

грант РФФИ

Этапы НИР

# Сроки Название
1 1 января 2013 г.-31 декабря 2013 г. Средства автоматической проверки темпоральных свойств асинхронных систем взаимодействующих процессов
Результаты этапа:
2 14 марта 2014 г.-31 декабря 2014 г. Средства автоматической проверки темпоральных свойств асинхронных систем взаимодействующих процессов
Результаты этапа: Разработана система верификации программно-конфигурируемых сетей (ПКС) в режиме реального времени, или динамической верификации. Ключевыми особенностями ПКС являются наличие централизованного управления сетью и однородность сети. Первая особенность достигается введением в сеть контроллера - объекта, связанного со всеми коммутаторами сети посредством виртуальных управляющих каналов связи. Контроллер может быть реализован многими различными способами, например, как особый узел сети или как программное обеспечение на каком-либо вычислительном устройстве, доступном для всех коммутаторов сети. Вторая особенность - однородность сети - состоит в том, что коммутаторы представляют собой вычислительные устройства, действующие по одинаковым принципам. в каждом из коммутаторов содержится таблица правил, определяющих, каким образом приходящие на коммутатор пакеты будут обрабатываться и перенаправляться дальше в сеть. Контроллер управляет заполнением таблиц коммутации, посылая различные команды коммутаторам по каналам связи, такие как команды вставки, удаления или модификации правил, и реагирует на события, происходящие в сети, такие как истечение срока действия правил или изменение топологии сети. В основе разработанного средства лежит модель, рассматривающая сеть как совокупность отношений, описывающих коммутацию пакетов. Отношения строятся над множеством состояний пакетов. Состояние пакета включает в себя имя коммутатора, его порт и (конечную) информацию о заголовке пакета и тем самым полностью определяет дальнейший маршрут, проходимый пакетом в сети. Так как разработанное нами средство предназначено для динамической верификации сети, модель, используемая в средстве, должна меняться в режиме реального времени, с тем чтобы в каждый момент времени адекватно описывать верифицируемую сеть. Нами разработаны эффективные алгоритмы такой модификации модели: средство встраивается в каналы управления между контроллером и коммутатором, отслеживает проходящие через эти каналы сообщения, извлекает из сообщений информацию об изменении модели сети и соответствующим образом эффективно изменяет модель. Средством проверяются свойства сети, описывающие политики маршрутизации сети в формализме логики предикатов первого порядка с транзитивным замыканием FO[TC]. Семантика этой логики определяется в терминах отношений, и тогда естественным образом описывается процесс верификации рассматриваемых политик маршрутизации: атомами являются базовые отношения модели, а логические связки переформулируются как операции над отношениями (дизъюнкция, конъюнкция, отрицание, кванторы становятся объединением, пересечением, дополнением, проекциями соответственно). Процесс верификации тогда можно формализовать как проверку того, является ли отношение, описываемое формулой, пустым для заданной модели сети. Если это не так, то политика маршрутизации считается нарушенной, и полученное отношение предоставляет информацию, которая может быть расценена как контрпример к проверяемой политике маршрутизации, то есть множество состояний пакетов, нарушающих эту политику. Эта информация может быть использована администратором сети для уточнения параметров сети с целью удовлетворения предъявляемых к сети политик маршрутизации. Предложенный ранее метод автоматической проверки темпоральных свойств ПКС применяется для верификации ПКС, параметризованных по временным параметрам, следующим образом. В модели ПКС учитываются временные аспекты системы, такие как задержка доставки пакетов по каналам сети, задержка обработки пакетов на коммутаторах. Модель описывается с помощью диаграмм UML и с помощью разработанного нами транслятора автоматически преобразуется во входную модель сети временных автоматов для верификатора UPPAAL и тем самым позволяет автоматически проверять свойства сети, выраженные темпоральными формулами логики TCTL. Трансляция организована таким образом, чтобы была справедлива особого вида бисимуляция между семантиками сети в исходной и результирующей модели, описанными как системы переходов: одному шагу вычисления исходной модели соответствует последовательность шагов в результирующей системе, и последовательности шагов между выделенными состояниями вычисления результирующей системы соответствует шаг вычисления исходной системы. Корректность алгоритма трансляции основывается на существовании такой бисимуляции. Размер системы автоматов линейно зависит от размера исходной системы, и кроме того, сама трансляция имеет довольно простой вид переписывания примитивов одной модели в примитивы другой модели, и этим обосновывается низкая сложность алгоритма трансляции. Свойства формализованной в нашей модели ПКС могут быть проверены для любых конкретных значений параметров. Если какие-либо из проверяемых для системы свойств нарушаются, могут быть произведены уточнение параметров и повторная проверка свойств, и так до тех пор, пока уточняемые параметры не будут удовлетворят предъявляемым к сети требованиям. Формальная верификация в целом и формальная верификация параметризованных моделей в частности есть проверка того, удовлетворяет ли описание модели формально специфицированным свойствам. Задача верификации, как правило, определяется для моделей вычислений: поведение объектов таких моделей (часто называемых программами) определяется как пошаговое изменение вычислительных конфигураций. Спецификация может рассматриваться как описание поведения идеальной программы, и тогда задача верификации состоит в том, чтобы проверить эквивалентность поведений идеальной и реальной программ. Это показывает важность исследования проблемы эквивалентности программ во всевозможных моделях вычислений: эффективные алгоритмы проверки эквивалентности программ могут быть использованы при составлении алгоритмов верификации. Нами были разработаны эффективные алгоритмы проверки эквивалентности для модели последовательных программ, в семантике которых учитываются свойства перестановочности операторов (результат применения операторов к текущей конфигурации не зависит от порядка их применения) и подавления операторов (применение заданного оператора фиктивно, если вслед за ним выполняется другой заданный оператор).
3 13 марта 2015 г.-31 декабря 2015 г. Средства автоматической проверки темпоральных свойств асинхронных систем взаимодействующих процессов
Результаты этапа:

Прикрепленные к НИР результаты

Для прикрепления результата сначала выберете тип результата (статьи, книги, ...). После чего введите несколько символов в поле поиска прикрепляемого результата, затем выберете один из предложенных и нажмите кнопку "Добавить".