Введение

Проверка во время выполнения – это подход к анализу и исполнению вычислительных систем, основанный на извлечении информации из работающей системы и использовании её для обнаружения и, возможно, реагирования на наблюдаемое поведение, удовлетворяющее или нарушающее заданные свойства. Некоторые специфические свойства, такие как отсутствие гонок данных и взаимных блокировок, обычно желательно обеспечить во всех системах и их можно наиболее эффективно реализовать алгоритмически. Другие свойства удобнее задавать в виде формальных спецификаций. Спецификации для проверки во время выполнения обычно выражаются с помощью формализмов предикатов трасс, таких как конечные автоматы, регулярные выражения, контекстно-свободные шаблоны, линейная временная логика и т.п., или их расширения. Это позволяет использовать менее эмпирический подход, чем при обычном тестировании. Однако, любой механизм мониторинга исполняющейся системы считается проверкой во время выполнения, включая проверку на соответствие тестовым оракулам и эталонным реализациям. При наличии формальных спецификаций требований, на их основе синтезируются мониторы, которые внедряются в систему посредством инструментации. Проверка во время выполнения может применяться для различных целей, таких как мониторинг политик безопасности, отладка, тестирование, верификация, валидация, профилирование, защита от сбоев, изменение поведения (например, восстановление) и т.д. Проверка во время выполнения позволяет избежать сложности традиционных методов формальной верификации, таких как проверка моделей и доказательство теорем, за счет анализа лишь одной или нескольких трасс исполнения и работы непосредственно с реальной системой, что обеспечивает хорошую масштабируемость и повышает уверенность в результатах анализа (поскольку исключается трудоёмкий и подверженный ошибкам этап формального моделирования системы), но при этом снижается полнота охвата. Более того, благодаря своим рефлексивным возможностям, проверка во время выполнения может стать неотъемлемой частью целевой системы, осуществляя мониторинг и управление её исполнением в процессе развёртывания.

Примеры

Примеры, приведенные ниже, рассматривают некоторые простые свойства, которые к моменту написания (апрель 2011 года) были изучены несколькими группами, занимающимися верификацией во время выполнения, возможно, с небольшими вариациями. Чтобы сделать их более интересными, каждое из свойств ниже использует различный формализм спецификации, и все они являются параметрическими. Параметрические свойства – это свойства трасс, формируемых параметрическими событиями, которые привязывают данные к параметрам. В данном случае параметрическое свойство имеет вид , где – это спецификация в некотором подходящем формализме, ссылающаяся на обобщенные (неинстанцированные) параметрические события. Идея таких параметрических свойств заключается в том, что свойство, выраженное , должно выполняться для всех экземпляров параметров, встречающихся (через параметрические события) в наблюдаемой трассе. Ни один из следующих примеров не предназначен для какой-либо конкретной системы верификации во время выполнения, хотя поддержка параметров, очевидно, необходима. В приведенных примерах предполагается синтаксис Java, таким образом, "==" обозначает логическое равенство, а "=" – присваивание. Некоторые методы (например, update в UnsafeEnumExample) являются вспомогательными методами, не входящими в состав API Java, и используются для наглядности.

Затем

Интерфейс Java Iterator требует, чтобы метод `hasNext` был вызван и возвращал `true` перед вызовом метода `next`. Если этого не произойдет, очень вероятно, что пользователь выйдет за пределы коллекции при итерации. На рисунке справа показана машина с конечным числом состояний, определяющая возможный монитор для проверки и обеспечения соблюдения этого свойства во время выполнения. Из неизвестного состояния вызов метода `next` всегда является ошибкой, поскольку такая операция может быть небезопасной. Если метод `hasNext` вызван и возвращает `true`, вызов `next` безопасен, поэтому монитор переходит в состояние `more`. Однако, если метод `hasNext` возвращает `false`, элементы отсутствуют, и монитор переходит в состояние `none`. В состояниях `more` и `none` вызов метода `hasNext` не предоставляет новой информации. Вызов метода `next` из состояния `more` безопасен, но состояние существования дополнительных элементов становится неизвестным, поэтому монитор возвращается в исходное неизвестное состояние. Наконец, вызов метода `next` из состояния `none` приводит к переходу в состояние ошибки. Далее представлено описание этого свойства с использованием параметрической логики линейного времени, ориентированной на прошлое. Эта формула утверждает, что любому вызову метода `next` должен непосредственно предшествовать вызов метода `hasNext`, возвращающий `true`. Свойство параметризовано относительно итератора `i`. Концептуально это означает, что в тестовой программе будет создана одна копия монитора для каждого возможного итератора, хотя системы проверки во время выполнения не обязаны реализовывать свои параметрические мониторы таким образом. Монитор для этого свойства будет настроен на запуск обработчика при нарушении формулы (что эквивалентно переходу машины с конечным числом состояний в состояние ошибки), что произойдет, если `next` будет вызван без предварительного вызова `hasNext`, или если `hasNext` будет вызван перед `next`, но вернет `false`.

НебезопасныйEnum

Класс Vector в Java имеет два способа итерации по своим элементам. Можно использовать интерфейс Iterator, как показано в предыдущем примере, или интерфейс Enumeration. Помимо добавления метода удаления для интерфейса Iterator, основное отличие заключается в том, что Iterator работает по принципу "fail-fast", а Enumeration – нет. Это означает, что если вектор изменяется (не с помощью метода remove интерфейса Iterator) во время итерации по нему с использованием Iterator, будет выброшено исключение ConcurrentModificationException. Однако при использовании Enumeration этого не происходит, как уже упоминалось. Это может привести к недетерминированным результатам работы программы, поскольку вектор окажется в несогласованном состоянии с точки зрения Enumeration. Для устаревших программ, которые по-прежнему используют интерфейс Enumeration, может потребоваться запретить использование Enumeration при изменении базового вектора. Для обеспечения такого поведения можно использовать следующую параметрическую регулярную схему:

∀ Вектор v, Перечисление e: (e = v.elements) (e.nextElement)* v.update e.nextElement

Эта схема параметрична как по отношению к Перечислению, так и к Вектору. Интуитивно, и как указано выше, системы проверки во время выполнения не обязаны реализовывать свои параметрические мониторы таким образом. Можно представить параметрический монитор для этого свойства как создающий и отслеживающий непараметрический экземпляр монитора для каждой возможной пары Вектора и Перечисления. Некоторые события могут затрагивать несколько мониторов одновременно, например, v.update, поэтому система проверки во время выполнения должна (опять же, концептуально) направлять их всем заинтересованным мониторам. Здесь свойство определено таким образом, чтобы описывать нежелательное поведение программы. Следовательно, это свойство должно отслеживаться на соответствие схеме. Рисунок справа показывает код Java, который соответствует этой схеме и, следовательно, нарушает свойство. Вектор v обновляется после создания перечисления e, а затем используется e.

Безопасный замок

Два предыдущих примера демонстрируют свойства конечных автоматов, но свойства, используемые при верификации во время выполнения, могут быть гораздо сложнее. Свойство SafeLock обеспечивает соблюдение политики, согласно которой количество операций захвата (acquire) и освобождения (release) блокировки (reentrant Lock) совпадает в пределах одного вызова метода. Это, разумеется, запрещает освобождение блокировки в методах, отличных от тех, где она была захвачена, но это вполне может быть желательным поведением для тестируемой системы. Ниже приведена спецификация этого свойства с использованием параметрической контекстно-свободной модели:

∀ Thread t, Lock l: S→ε | S begin(t) S end(t) | S l. acquire(t) S l. release(t)

Эта модель определяет сбалансированные последовательности вложенных пар "начало/конец" и "захват/освобождение" для каждого потока (Thread) и каждой блокировки (Lock) (где S – пустая последовательность). Здесь "начало" и "конец" относятся к началу и концу каждого метода в программе (за исключением самих вызовов захвата и освобождения). Они параметризованы по потоку, поскольку необходимо связывать начало и конец методов только в том случае, если они принадлежат одному и тому же потоку. События захвата и освобождения также параметризованы по потоку по той же причине. Кроме того, они параметризованы по блокировке, поскольку мы не хотим связывать освобождение одной блокировки с захватом другой. В крайнем случае, может потребоваться экземпляр свойства, то есть копия механизма контекстно-свободного разбора, для каждой возможной комбинации потока и блокировки; это происходит, опять же, интуитивно, потому что системы верификации во время выполнения могут реализовывать одну и ту же функциональность по-разному. Например, если система имеет потоки , , и с блокировками и , то может потребоваться поддерживать экземпляры свойств для пар <,>, <,>, <,>, <,>, <,>, и <,>. Это свойство должно контролироваться на предмет несоответствия шаблону, поскольку шаблон определяет корректное поведение. Рисунок справа показывает трассу, которая приводит к двум нарушениям этого свойства. Шаги вниз на рисунке представляют начало метода, а шаги вверх – его конец. Серые стрелки на рисунке показывают соответствие между конкретными операциями захвата и освобождения одной и той же блокировки. Для простоты трасса показывает только один поток и одну блокировку.

Исследовательские задачи и применение

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

Сокращение накладных расходов на время выполнения

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

Улучшенная инструментация. Извлечение событий из исполняющейся системы и отправка их в мониторы может создавать значительные накладные расходы на время выполнения, если это сделано без должной оптимизации. Качественная инструментация системы критически важна для любого инструмента верификации во время выполнения, если только инструмент явно не предназначен для работы с существующими логами выполнения. В настоящее время используется множество подходов к инструментации, каждый из которых имеет свои преимущества и недостатки: от пользовательской или ручной инструментации до специализированных библиотек, компиляции в языки, ориентированные на аспекты, расширения виртуальной машины и использования аппаратной поддержки. Комбинирование со статическим анализом. Распространенная комбинация статического и динамического анализа, особенно часто встречающаяся в компиляторах, заключается в мониторинге всех требований, которые не могут быть удовлетворены статически. В верификации во время выполнения все чаще используется двойной и, в конечном счете, эквивалентный подход – применение статического анализа для уменьшения объема мониторинга, который в противном случае был бы исчерпывающим. Статический анализ может быть применен как к проверяемому свойству, так и к самой системе. Статический анализ свойства, подлежащего мониторингу, может выявить, что некоторые события не требуют мониторинга, создание определенных мониторов можно отложить, а некоторые существующие мониторы никогда не будут активированы и, следовательно, могут быть удалены сборщиком мусора. Статический анализ системы, подлежащей мониторингу, может обнаружить код, который никогда не сможет повлиять на мониторы. Например, при мониторинге свойства HasNext, нет необходимости инструментировать части кода, где каждый вызов i.next непосредственно следует за вызовом i.hasNext, возвращающим true (что видно на графе потока управления). Эффективная генерация и управление мониторами. При мониторинге параметрических свойств, таких как те, что приведены в примерах выше, система мониторинга должна отслеживать состояние контролируемого свойства для каждого экземпляра параметра. Теоретически количество таких экземпляров не ограничено и на практике может быть огромным. Важной исследовательской задачей является эффективная отправка наблюдаемых событий только тем экземплярам, которым они необходимы. Связанная задача – уменьшение количества таких экземпляров (для ускорения отправки), другими словами, избежание создания ненужных экземпляров как можно дольше и, наоборот, удаление уже созданных экземпляров, как только они становятся ненужными. Наконец, алгоритмы параметрического мониторинга обычно обобщают аналогичные алгоритмы для генерации непараметрических мониторов. Таким образом, качество генерируемых непараметрических мониторов определяет качество получаемых параметрических мониторов. Однако, в отличие от других подходов к верификации (например, проверки моделей), количество состояний или размер генерируемого монитора менее важны в верификации во время выполнения; некоторые мониторы могут иметь бесконечное число состояний, например, монитор для свойства SafeLock, хотя в любой момент времени может быть достигнуто только конечное число состояний. Важно, насколько эффективно монитор переходит из одного состояния в следующее при получении события от исполняющейся системы.

Указывающие свойства

Одним из основных практических препятствий всех формальных подходов является то, что пользователи неохотно берутся за чтение и написание спецификаций, либо не знают, как это делать, и не хотят учиться. В некоторых случаях спецификации неявны, например, в отношении взаимных блокировок и гонок данных, но в большинстве случаев их необходимо создавать. Дополнительным неудобством, особенно в контексте верификации во время выполнения, является то, что многие существующие языки спецификаций недостаточно выразительны для описания требуемых свойств. Необходимы более совершенные формализмы. Значительные усилия в сообществе верификации во время выполнения направлены на разработку формализмов спецификаций, которые лучше соответствуют целевым областям применения, чем традиционные формализмы. Некоторые из них включают незначительные или отсутствующие синтаксические изменения традиционных формализмов, но затрагивают их семантику (например, семантику конечных и бесконечных трасс) и реализацию (оптимизированные конечные автоматы вместо автоматов Бюхи). Другие расширяют существующие формализмы функциями, которые хорошо подходят для верификации во время выполнения, но могут быть менее удобны для других подходов к верификации, например, добавлением параметров, как показано в приведенных выше примерах. Наконец, существуют формализмы спецификаций, разработанные специально для верификации во время выполнения, стремящиеся к оптимальной производительности в этой области и не уделяющие особого внимания другим областям применения. Разработка более совершенных универсальных или предметно-ориентированных формализмов спецификаций для верификации во время выполнения является и останется одной из ключевых исследовательских задач. Количественные свойства. По сравнению с другими подходами к верификации, верификация во время выполнения позволяет оперировать конкретными значениями переменных состояния системы, что дает возможность собирать статистическую информацию о выполнении программы и использовать ее для оценки сложных количественных свойств. Требуются более выразительные языки спецификаций, которые позволят в полной мере использовать эту возможность. Улучшенные интерфейсы. Чтение и написание спецификаций нелегко для неспециалистов. Даже эксперты часто подолгу рассматривают относительно небольшие формулы темпоральной логики (особенно с вложенными операторами "until"). Важным направлением исследований является разработка мощных пользовательских интерфейсов для различных формализмов спецификаций, которые облегчат пользователям понимание, написание и, возможно, даже визуализацию свойств. Извлечение спецификаций. Независимо от доступной инструментальной поддержки, пользователи почти всегда предпочтут не писать спецификации вообще, особенно если они тривиальны. К счастью, существует множество программ, которые, как предполагается, корректно используют действия/события, для которых требуется определить свойства. В этом случае было бы полезно использовать эти корректные программы для автоматического извлечения требуемых свойств. Даже если ожидается, что качество автоматически извлеченных спецификаций будет ниже, чем у созданных вручную, они могут служить отправной точкой для последних или основой для автоматических инструментов верификации во время выполнения, предназначенных специально для поиска ошибок (где некачественная спецификация приводит к ложноположительным или ложноотрицательным результатам, что часто допустимо при тестировании).

Модели исполнения и прогнозный анализ

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

Изменение поведения

В отличие от тестирования или исчерпывающей верификации, проверка во время выполнения позволяет надеяться на возможность восстановления системы после обнаруженных нарушений посредством переконфигурации, микроперезагрузок или более тонких механизмов вмешательства, иногда называемых настройкой или управлением. Реализация этих техник в строгом контексте проверки во время выполнения порождает дополнительные задачи. Спецификация действий. Необходимо определить модификацию, которую следует выполнить, в достаточно абстрактной форме, чтобы пользователю не требовалось знание несущественных деталей реализации. Кроме того, необходимо указать, когда эта модификация может быть применена, чтобы обеспечить целостность системы. Обоснование эффектов вмешательства. Важно убедиться, что вмешательство улучшает ситуацию или, по крайней мере, не ухудшает её. Интерфейсы действий. Подобно инструментам для мониторинга, необходимо обеспечить возможность получения системой запросов на выполнение действий. Механизмы запроса неизбежно будут зависеть от деталей реализации системы. Однако на уровне спецификации необходимо предоставить пользователю декларативный способ предоставления обратной связи системе, определяя, какие действия следует применять и при каких условиях.

Ориентированное на аспекты программирование

Исследователи в области Runtime Verification осознали потенциал использования аспектно-ориентированного программирования (AOP) как метода модульного определения программной инструментации. Аспектно-ориентированное программирование (AOP) в целом способствует модульности сквозных задач. Runtime Verification по своей природе является одной из таких задач и, следовательно, может воспользоваться определенными свойствами AOP. Определения мониторов, основанных на аспектах, в значительной степени являются декларативными и, как следствие, обычно проще для понимания, чем инструментация, выраженная посредством преобразования программы, написанной на императивном языке программирования. Более того, статический анализ может легче анализировать аспекты мониторинга, чем другие формы программной инструментации, поскольку вся инструментация содержится в одном аспекте. Многие современные инструменты Runtime Verification реализованы в виде компиляторов спецификаций, которые принимают на вход выразительную спецификацию высокого уровня и генерируют на выходе код, написанный на некотором языке аспектно-ориентированного программирования (например, AspectJ).

Сочетание с формальной проверкой

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

Расширение охвата

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

Генерация входных данных. Хорошо известно, что создание хорошего набора входных данных (значения входных переменных программы, значения системных вызовов, расписания потоков и т. д.) может значительно повысить эффективность тестирования. Это справедливо и для верификации во время выполнения, используемой для обнаружения ошибок, но в дополнение к использованию программного кода для управления процессом генерации входных данных, в верификации во время выполнения можно также использовать спецификации свойств, когда они доступны, а также использовать методы мониторинга для стимулирования желаемого поведения. Это использование верификации во время выполнения делает её тесно связанной с тестированием на основе моделей, хотя спецификации верификации во время выполнения обычно имеют общее назначение и не обязательно разрабатываются для целей тестирования. Например, если требуется протестировать свойство UnsafeEnum общего назначения, описанное выше, вместо простой генерации упомянутого выше монитора для пассивного наблюдения за выполнением системы, можно создать более интеллектуальный монитор, который замораживает поток, пытающийся сгенерировать второе событие e.nextElement (непосредственно перед его генерацией), позволяя другим потокам выполняться в надежде, что один из них сгенерирует событие v.update, в этом случае ошибка будет обнаружена. Динамическое символическое выполнение. В символическом выполнении программы выполняются и контролируются символически, то есть без конкретных входных данных. Одно символическое выполнение системы может охватывать большой набор конкретных входных данных. Для управления символическими выполнениями или систематического исследования их пространства часто используются стандартные методы решения ограничений или проверки выполнимости. Если базовые решатели выполнимости не могут обработать точку выбора, то может быть сгенерирован конкретный вход для прохождения этой точки; эта комбинация конкретного и символического выполнения также называется конколической (concolic) верификацией.