|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ФИЦ ПХФ и МХ РАН |
||
Средства автоматической проверки темпоральных свойств асинхронных систем взаимодействующих процессовНИР
- Руководитель НИР: Чистолинов М.В.
- Участники НИР: Балашов В.В., Герасёв А.В., Подымов В.В., Попеско У.В.
- Подразделение: Лаборатория вычислительных комплексов
- Срок исполнения: 1 января 2013 г. - 31 декабря 2015 г.
- Номер договора (контракта, соглашения): 13-07-00669-а
- Номер ЦИТИС: 01201356241
- Тип: Фундаментальная
- Приоритетное направление научных исследований: Информационные технологии, компьютерные сети, распределенные вычисления и защита информации
- ПН России: Информационно-телекоммуникационные системы
- Направление технологического прорыва России: Стратегические информационные технологии
-
Рубрики ГРНТИ:
- 27.03.19 Математическая логика
- 50.05.03 Общетеоретические вопросы программирования
-
Ключевые слова:
итеративное построение инвариантов, размеченные системы переходов
-
Описание:
В рамках проекта предполагается разработка методов и средств решения задачи верификации параметризованных моделей для класса реагирующих систем, удовлетворяющих следующим ограничениям: 1) в системе используется асинхронный параллелизм; 2) процессы взаимодействуют посредством передачи сообщений; 3) коммуникационная топология системы фиксируется для каждой системы и описывается регулярным образом; 4) процессы порождаются на основе заданного конечного множества прототипов; 5) процессы и каналы связи считаются надёжными; 6) свойства реагирующей системы и моделей параметризованного семейства описываются при помощи логики линейного времени. В ходе выполнения проекта планируется решить следующие задачи: - разработать алгоритмы построения отношений симуляции с учётом симметричности проверяемых моделей; разработать алгоритмы построения контрпримеров, демонстрирующих нарушение требований симуляции; интегрировать разработанные алгоритмы в систему верификации параметризованных моделей. - провести экспериментальную проверку применимости разработанных алгоритмов; исследовать способы представления коммуникационной топологии и параметризованным системам, альтернативные сетевым грамматикам; - разработать итеративные алгоритмы поиска инвариантов с построением отношений симуляции и применением методов абстракции для заданных свойств; интегрировать разработанные алгоритмы в систему верификации параметризованных моделей.
-
Основные результаты:
За период работы по Проекту были получены следующие результаты: 1. Разработано средство верификации распределенных вычислительных систем реального времени (РВС РВ), состоящее из средства описания РВС РВ в виде диаграмм состояний универсального языка моделирования UML, средства верификации сетей (плоских) временных автоматов UPPAAL и разработанного и реализованного нами алгоритма трансляции диаграммы состояний в сеть временных автоматов. Доказана бисимуляция между поведениями исходной и транслированной моделями, и на её основе - корректность алгоритма трансляции. 2. Разработана модель программно-конфигурируемых сетей (ПКС), учитывающая временные характеристики сети. Предложен подход к автоматической верифицикации временных свойств сетей в этой модели, позволяющий уточнять их временные параметры. Разработан и реализован алгоритм трансляции предложенной модели ПКС в модель сети временных автоматов. Доказна бисимуляция между поведениями исходной и транслированной моделей, и на её основе - корректность алгоритма трансляции. 3. Разработано средство оперативной верификации программно-конфигурируемых сетей VERMONT, в основе которого лежит модель, рассматривающая сеть как совокупность отношений, описывающих коммутацию пакетов. 4. Разработан эффективный алгоритм проверки эквивалентности последовательных программ в моделях, семантика которых учитывает свойства перестановочности и подавления операторов.
- Добавил в систему: Чистолинов Максим Владимирович
Соисполнители НИР
| МГУ имени М.В.Ломоносова | Координатор |
Источник финансирования НИР
| грант РФФИ |
Этапы НИР
| # | Сроки | Название |
| 1 | 1 января 2013 г.-31 декабря 2013 г. | Средства автоматической проверки темпоральных свойств асинхронных систем взаимодействующих процессов |
| Результаты этапа: | ||
| 2 | 14 марта 2014 г.-31 декабря 2014 г. | Средства автоматической проверки темпоральных свойств асинхронных систем взаимодействующих процессов |
| Результаты этапа: Разработана система верификации программно-конфигурируемых сетей (ПКС) в режиме реального времени, или динамической верификации. Ключевыми особенностями ПКС являются наличие централизованного управления сетью и однородность сети. Первая особенность достигается введением в сеть контроллера - объекта, связанного со всеми коммутаторами сети посредством виртуальных управляющих каналов связи. Контроллер может быть реализован многими различными способами, например, как особый узел сети или как программное обеспечение на каком-либо вычислительном устройстве, доступном для всех коммутаторов сети. Вторая особенность - однородность сети - состоит в том, что коммутаторы представляют собой вычислительные устройства, действующие по одинаковым принципам. в каждом из коммутаторов содержится таблица правил, определяющих, каким образом приходящие на коммутатор пакеты будут обрабатываться и перенаправляться дальше в сеть. Контроллер управляет заполнением таблиц коммутации, посылая различные команды коммутаторам по каналам связи, такие как команды вставки, удаления или модификации правил, и реагирует на события, происходящие в сети, такие как истечение срока действия правил или изменение топологии сети. В основе разработанного средства лежит модель, рассматривающая сеть как совокупность отношений, описывающих коммутацию пакетов. Отношения строятся над множеством состояний пакетов. Состояние пакета включает в себя имя коммутатора, его порт и (конечную) информацию о заголовке пакета и тем самым полностью определяет дальнейший маршрут, проходимый пакетом в сети. Так как разработанное нами средство предназначено для динамической верификации сети, модель, используемая в средстве, должна меняться в режиме реального времени, с тем чтобы в каждый момент времени адекватно описывать верифицируемую сеть. Нами разработаны эффективные алгоритмы такой модификации модели: средство встраивается в каналы управления между контроллером и коммутатором, отслеживает проходящие через эти каналы сообщения, извлекает из сообщений информацию об изменении модели сети и соответствующим образом эффективно изменяет модель. Средством проверяются свойства сети, описывающие политики маршрутизации сети в формализме логики предикатов первого порядка с транзитивным замыканием FO[TC]. Семантика этой логики определяется в терминах отношений, и тогда естественным образом описывается процесс верификации рассматриваемых политик маршрутизации: атомами являются базовые отношения модели, а логические связки переформулируются как операции над отношениями (дизъюнкция, конъюнкция, отрицание, кванторы становятся объединением, пересечением, дополнением, проекциями соответственно). Процесс верификации тогда можно формализовать как проверку того, является ли отношение, описываемое формулой, пустым для заданной модели сети. Если это не так, то политика маршрутизации считается нарушенной, и полученное отношение предоставляет информацию, которая может быть расценена как контрпример к проверяемой политике маршрутизации, то есть множество состояний пакетов, нарушающих эту политику. Эта информация может быть использована администратором сети для уточнения параметров сети с целью удовлетворения предъявляемых к сети политик маршрутизации. Предложенный ранее метод автоматической проверки темпоральных свойств ПКС применяется для верификации ПКС, параметризованных по временным параметрам, следующим образом. В модели ПКС учитываются временные аспекты системы, такие как задержка доставки пакетов по каналам сети, задержка обработки пакетов на коммутаторах. Модель описывается с помощью диаграмм UML и с помощью разработанного нами транслятора автоматически преобразуется во входную модель сети временных автоматов для верификатора UPPAAL и тем самым позволяет автоматически проверять свойства сети, выраженные темпоральными формулами логики TCTL. Трансляция организована таким образом, чтобы была справедлива особого вида бисимуляция между семантиками сети в исходной и результирующей модели, описанными как системы переходов: одному шагу вычисления исходной модели соответствует последовательность шагов в результирующей системе, и последовательности шагов между выделенными состояниями вычисления результирующей системы соответствует шаг вычисления исходной системы. Корректность алгоритма трансляции основывается на существовании такой бисимуляции. Размер системы автоматов линейно зависит от размера исходной системы, и кроме того, сама трансляция имеет довольно простой вид переписывания примитивов одной модели в примитивы другой модели, и этим обосновывается низкая сложность алгоритма трансляции. Свойства формализованной в нашей модели ПКС могут быть проверены для любых конкретных значений параметров. Если какие-либо из проверяемых для системы свойств нарушаются, могут быть произведены уточнение параметров и повторная проверка свойств, и так до тех пор, пока уточняемые параметры не будут удовлетворят предъявляемым к сети требованиям. Формальная верификация в целом и формальная верификация параметризованных моделей в частности есть проверка того, удовлетворяет ли описание модели формально специфицированным свойствам. Задача верификации, как правило, определяется для моделей вычислений: поведение объектов таких моделей (часто называемых программами) определяется как пошаговое изменение вычислительных конфигураций. Спецификация может рассматриваться как описание поведения идеальной программы, и тогда задача верификации состоит в том, чтобы проверить эквивалентность поведений идеальной и реальной программ. Это показывает важность исследования проблемы эквивалентности программ во всевозможных моделях вычислений: эффективные алгоритмы проверки эквивалентности программ могут быть использованы при составлении алгоритмов верификации. Нами были разработаны эффективные алгоритмы проверки эквивалентности для модели последовательных программ, в семантике которых учитываются свойства перестановочности операторов (результат применения операторов к текущей конфигурации не зависит от порядка их применения) и подавления операторов (применение заданного оператора фиктивно, если вслед за ним выполняется другой заданный оператор). | ||
| 3 | 13 марта 2015 г.-31 декабря 2015 г. | Средства автоматической проверки темпоральных свойств асинхронных систем взаимодействующих процессов |
| Результаты этапа: | ||
Прикрепленные к НИР результаты
Для прикрепления результата сначала выберете тип результата (статьи, книги, ...). После чего введите несколько символов в поле поиска прикрепляемого результата, затем выберете один из предложенных и нажмите кнопку "Добавить".