Константин Савенков / Ампилогов Антон, 4 курс, sec-sem

На этом форуме публикуются и уточняются постановки задач студентам, а также отслеживается ход их выполнения

Модератор: staff

Закрыто
Бычков Иван
Аспирант
Сообщения: 179
Зарегистрирован: 23 сен 2008 01:19 pm

Константин Савенков / Ампилогов Антон, 4 курс, sec-sem

Сообщение Бычков Иван »

Тема

Динамическая проверка свойств поведения вычислительных систем
.
Формулировки проблемы

В прошлом году был разработан подход к динамической проверке свойств темпоральной логики LTL в СОА RedSecure. Идея подхода заключается в том, что формула LTL транслируется в альтернирующий автомат (АА), по которому строится распознающий автомат на языке Aura, используемый в СОА RedSecure для описания распознающих анализаторов.

Для построения АА использовался известный алгоритм, основная исследовательская составляющая касалась построения распознающего автомата. Дело в том, что реализация альтернирующих автоматов в Aura/RedSecure неэффективна с точки зрения производительности и затрат памяти. Для эффективной работы распознавателя пришлось разработать алгоритм, строящий по АА недетерминированный конечный автомат (НКА). Фактически, данный алгоритм выполняет линеаризацию АА.

В текущем году предполагается продолжить повышение эффективности разработанного решения. Так, при линеаризации АА в общем случае происходит экспоненциальный рост количества состояний НКА. Предполагается модернизировать алгоритм проверки так, чтобы развёртка АА в НКА происходила динамически, во время выполнения динамической проверки, подобно тому, как выполняется on-the-fly model checking.

Также планируется исследование вопроса корректности разработанных алгоритмов.

План работ

TBD

Ожидаемые результаты

1. Модернизированный алгоритм динамической проверки свойств LTL при помощи альтернирующих автоматов.
2. Подготовка статьи на тему динамической линеаризации альтернирующих автоматов.
3. Прототип программного средства, позволяющего описывать и динамически проверять выполнимость свойств LTL на трассах работы приложения в среде Linux (совместно с Денисом Гамаюновым, Андреем Сапожниковым, Татьяной Горнак).
4. Подготовка совместной статьи, посвящённой инструментальной системе мониторинга и динамической верификации поведения приложений в ОС Linux.
Антон Ампилогов
Выпускник
Сообщения: 2
Зарегистрирован: 16 дек 2008 10:34 pm

Отчет о проделанной работе

Сообщение Антон Ампилогов »

Тема

Динамическая верификация программ во время выполнения.

Цель работы

Сделать возможной динамическую проверку свойств, описанных на LTL, осуществляемую в рамках СОА «RedSecure»

Актуальность

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

Постановка задачи

Модернизация алгоритма таким образом, что проверка LTL формул будет осуществляться
при помощи одного автомата на Aura, который будет моделировать детерминированный
конечный автомат.

Усовершенствование алгоритма и прототипа таким образом, чтобы была возможна проверка
свойств tLTL.

Создание совместно с другими студентами программного средства, осуществляющего контроль поведения приложений, работающих на машинах с ОС
Linux.

Написание статьи описывающей подход.

Проделанная работа

Разработанный в прошлом году алгоритм был модернизирован. В новом алгоритме нужен всего один автомат на языке Aura для проверки формул LTL, раньше формула LTL проверялась при помощи нескольких автоматов на языке Aura, связь
между ними осуществлялась при помощи событий порождаемых средствами
RedSecure.

Решен вопрос с ограниченностью места занимаемого автоматами проверяющими формулы LTL .
Возможна оценка места занимаемого автоматом. И ускорено вычисление обработки очередного события, получаемого от системы мониторинга, за счет того, что теперь не нужны дополнительные события для связи между автоматами, а так же использования двоичного представления ДНФ, описывающих состояние моделируемого детерминированного автомата.

Написан прототип по новому алгоритму.

Написана статья по разработанному подходу.

Ведется работа над возможностью проверки свойств tLTL.
На данный момент возможно два подхода:
1. модернизация существующего подхода, добавлением в него обработки операторов
которыми tLTL отличается от LTL;

2. программно реализовать подход, описанный в статье Runime Verification of Timed
LTL using Disjunctive Normalized Equation System.

Предпочтительным является первый поход.
Закрыто