Проверка во время выполнения - Runtime verification

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

История и контекст

Проверка формально или неофициально указанных свойств на соответствие выполняемым системам или программам - старая тема (примечательными примерами являются динамическая типизация в программном обеспечении, или отказоустойчивых устройствах, или сторожевых таймерах в оборудовании), точные корни которых трудно определить. Терминология проверка во время выполнения был официально представлен как название семинара 2001 г.^[2] направлен на решение проблем на границе между формальной верификацией и тестированием. Для больших баз кода ручное написание тестовых примеров занимает очень много времени. Кроме того, не все ошибки можно обнаружить во время разработки. Ранний вклад в автоматизацию проверки был сделан в Исследовательском центре Эймса НАСА Клаусом Хавелундом и Григоре Росу сохранить высокие стандарты безопасности в космических аппаратах, вездеходах и авионике.^[3] Они предложили инструмент для проверки спецификаций в темпоральной логике и обнаружения условия гонки и тупиковые ситуации в программах Java путем анализа отдельных путей выполнения.

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

В широкой области проверки времени выполнения можно выделить несколько категорий, таких как:

мониторинг «без спецификаций», нацеленный на фиксированный набор свойств, в основном связанных с параллелизмом, таких как атомарность. Новаторская работа в этой области принадлежит Savage. и другие. с алгоритмом Eraser^[4]
мониторинг в отношении спецификаций временной логики; Ранний вклад в это направление был сделан Ли, Каннаном и их сотрудниками,^[5]^[6] и Хавелунд и Рошу.^[7]^[8]

Основные подходы

Обзор процесса проверки на основе монитора, описанный Havelund et al. в Учебное пособие по проверке во время выполнения.

Широкий спектр методов проверки во время выполнения можно классифицировать по трем параметрам:^[9]

Систему можно контролировать во время самого выполнения (онлайн) или после выполнения, например. в форме анализ журнала (не в сети).
Проверочный код интегрирован в систему (как это сделано в Аспектно-ориентированное программирование ) или предоставляется как внешний объект.
Монитор может сообщить о нарушении или проверке желаемой спецификации.

Тем не менее, основной процесс проверки во время выполнения остается аналогичным:^[9]

Монитор создается из какой-то формальной спецификации. Этот процесс обычно может быть выполнен автоматически, если существует эквивалентный автомат для формального языка, на котором указано свойство. Чтобы преобразовать регулярное выражение а конечный автомат может быть использован; недвижимость в линейная темпоральная логика может быть преобразован в Büchi автомат (смотрите также Линейная темпоральная логика к автомату Бюхи ).
Система оснащена инструментами для отправки на монитор событий, касающихся ее состояния выполнения.
Система запускается и проверяется монитором.
Монитор проверяет полученную трассировку событий и выносит вердикт, удовлетворены ли спецификации. Кроме того, монитор отправляет в систему обратную связь, чтобы исправить ложное поведение. При использовании автономного мониторинга система причины не может получать никакой обратной связи, поскольку проверка выполняется позже.

Примеры

В приведенных ниже примерах обсуждаются некоторые простые свойства, которые были рассмотрены, возможно, с небольшими вариациями, несколькими группами проверки времени выполнения на момент написания этой статьи (апрель 2011 г.). Чтобы сделать их более интересными, каждое свойство ниже использует другой формализм спецификации, и все они параметрические. Параметрические свойства - это свойства трассировок, сформированных с помощью параметрических событий, которые являются событиями, связывающими данные с параметрами. Здесь параметрическое свойство имеет вид ${ displaystyle forall parameters: varphi}$ , куда ${ displaystyle varphi}$ - это спецификация в некотором подходящем формализме, относящаяся к общим (неустановленным) параметрическим событиям. Интуиция для таких параметрических свойств заключается в том, что свойство, выраженное ${ displaystyle varphi}$ должен сохраняться для всех экземпляров параметров, встречающихся (через параметрические события) в наблюдаемой трассе. Ни один из следующих примеров не относится к какой-либо конкретной системе проверки времени выполнения, хотя поддержка параметров, очевидно, необходима. В следующих примерах предполагается синтаксис Java, поэтому «==» - это логическое равенство, а «=» - это присваивание. Некоторые методы (например, Обновить() в UnsafeEnumExample) - это фиктивные методы, которые не являются частью Java API и используются для ясности.

HasNext

Свойство HasNext

Ява Итератор интерфейс требует, чтобы hasNext () вызывается и возвращает истину перед следующий() вызывается метод. Если этого не происходит, вполне возможно, что пользователь будет повторять "с конца" Коллекция. На рисунке справа показан конечный автомат, который определяет возможный монитор для проверки и применения этого свойства с проверкой во время выполнения. От неизвестный состояние, всегда является ошибкой вызывать следующий() метод, потому что такая операция может быть небезопасной. Если hasNext () называется и возвращается истинный, можно позвонить следующий(), поэтому монитор входит в более государственный. Если, однако, hasNext () метод возвращает ложный, элементов больше нет, и монитор переходит в никто государственный. в более и никто государства, называя hasNext () метод не предоставляет новой информации. Можно с уверенностью назвать следующий() метод из более состояние, но становится неизвестным, если существует больше элементов, поэтому монитор повторно вводит начальное неизвестный государственный. Наконец, позвонив в следующий() метод из никто состояние приводит к попаданию в ошибка государственный. Далее следует представление этого свойства с использованием параметрического прошлого времени. линейная темпоральная логика.

${ displaystyle forall ~ { text {Iterator}} ~ i quad i. { text {next}} () ~ rightarrow ~ odot (i. { text {hasNext}} () == true) }$

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

UnsafeEnum

Код, нарушающий свойство UnsafeEnum

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

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

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

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

Трассировка, показывающая два нарушения свойства SafeLock.

Шаблон определяет сбалансированные последовательности вложенных пар начало / конец и получение / выпуск для каждого потока и блокировки ( ${ displaystyle epsilon}$ - пустая последовательность). Здесь begin и end относятся к началу и концу каждого метода в программе (кроме вызовов получения и освобождения самих себя). Они являются параметрическими в потоке, потому что необходимо связать начало и конец методов тогда и только тогда, когда они принадлежат одному потоку. События получения и выпуска также являются параметрическими в потоке по той же причине. Кроме того, они являются параметрическими в Lock, потому что мы не хотим связывать выпуски одного Lock с приобретениями другого. В крайнем случае, возможно, что будет экземпляр свойства, то есть копия механизма контекстно-свободного синтаксического анализа, для каждой возможной комбинации Thread с Lock; это происходит снова интуитивно, потому что системы проверки времени выполнения могут реализовывать одни и те же функции по-разному. Например, если в системе есть потоки ${ displaystyle t_ {1}}$ , ${ displaystyle t_ {2}}$ , и ${ displaystyle t_ {3}}$ с замками ${ displaystyle l_ {1}}$ и ${ displaystyle l_ {2}}$ , то можно поддерживать экземпляры свойств для пар < ${ displaystyle t_ {1}}$ , ${ displaystyle l_ {1}}$ >, < ${ displaystyle t_ {1}}$ , ${ displaystyle l_ {2}}$ >, < ${ displaystyle t_ {2}}$ , ${ displaystyle l_ {1}}$ >, < ${ displaystyle t_ {2}}$ , ${ displaystyle l_ {2}}$ >, < ${ displaystyle t_ {3}}$ , ${ displaystyle l_ {1}}$ > и < ${ displaystyle t_ {3}}$ , ${ displaystyle l_ {2}}$ >. Это свойство следует отслеживать на предмет сбоев в соответствии с шаблоном, поскольку шаблон определяет правильное поведение. На рисунке справа показан след, который вызывает два нарушения этого свойства. Шаги вниз на рисунке представляют собой начало метода, а шаги вверх - конец. Серые стрелки на рисунке показывают соответствие между полученными и выпусками одного и того же замка. Для простоты на трассировке показан только один поток и одна блокировка.

Проблемы исследования и приложения

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

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

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

Улучшенная аппаратура. Извлечение событий из исполняющей системы и их отправка на мониторы может привести к большим накладным расходам времени выполнения, если все сделано наивно. Хорошая системная инструментация имеет решающее значение для любого инструмента проверки времени выполнения, если только инструмент явно не нацелен на существующие журналы выполнения. В настоящее время используется множество инструментальных подходов, каждый из которых имеет свои преимущества и недостатки, начиная от настраиваемого или ручного инструментария и заканчивая специализированными библиотеками, компиляцией в аспектно-ориентированные языки, расширением виртуальной машины и поддержкой аппаратного обеспечения.
Сочетание со статическим анализом. Обычный^{[нужна цитата ]} Комбинация статического и динамического анализа, особенно встречающаяся в компиляторах, предназначена для отслеживания всех требований, которые не могут быть выполнены статически. Двойственный и в конечном итоге эквивалентный подход становится нормой^{[нужна цитата ]} при проверке во время выполнения, а именно использовать статический анализ чтобы уменьшить объем исчерпывающего мониторинга. Статический анализ может выполняться как на контролируемой собственности, так и на отслеживаемой системе. Статический анализ отслеживаемого свойства может выявить, что определенные события не нужно отслеживать, создание определенных мониторов может быть отложено, а некоторые существующие мониторы никогда не сработают и, следовательно, могут быть собраны мусором. Статический анализ отслеживаемой системы может обнаружить код, который никогда не повлияет на мониторы. Например, при мониторинге HasNext свойство выше, не нужны инструментальные части кода, где каждый вызов i.next () сразу же предшествует на любом пути вызов i.hasnext () который возвращается истинный (отображается на графике потока управления).
Эффективное создание мониторов и управление ими. При мониторинге параметрических свойств, подобных приведенным в примерах выше, системе мониторинга необходимо отслеживать состояние отслеживаемого свойства по отношению к каждому экземпляру параметра. Число таких случаев теоретически неограниченно и на практике имеет тенденцию быть огромным. Важная исследовательская задача состоит в том, как эффективно направлять наблюдаемые события именно тем экземплярам, которые в них нуждаются. Связанная с этим проблема заключается в том, как сохранить небольшое количество таких экземпляров (чтобы ускорить отправку), или, другими словами, как избежать создания ненужных экземпляров как можно дольше и, вдвойне, как удалить уже созданные экземпляры, как только они становятся ненужными. Наконец, алгоритмы параметрического мониторинга обычно обобщают аналогичные алгоритмы для создания непараметрических мониторов. Таким образом, качество созданных непараметрических мониторов диктует качество получаемых параметрических мониторов. Однако, в отличие от других подходов к проверке (например, проверка модели), количество состояний или размер сгенерированного монитора менее важны при проверке во время выполнения; на самом деле, у некоторых мониторов может быть бесконечно много состояний, например, для Безопасный замок свойство выше, хотя в любой момент времени могло произойти только конечное число состояний. Важно то, насколько эффективно монитор переходит из состояния в следующее состояние при получении события от исполняющей системы.

Определение свойств

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

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

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

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

Модификация поведения

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

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

Связанных с работой

Аспектно-ориентированное программирование

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

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

Проверка во время выполнения, если она используется в сочетании с доказуемо правильным кодом восстановления, может обеспечить бесценную инфраструктуру для проверки программ, которая может значительно снизить ее сложность. Например, формально проверить алгоритм сортировки кучи очень сложно. Менее сложным методом проверки является отслеживание сортировки вывода (монитор линейной сложности) и, если не сортировка, то сортировка с помощью некоторой легко проверяемой процедуры, например сортировки вставкой. Полученная программа сортировки теперь легче проверяется, единственное, что требуется от heap-sort, - это то, что она не уничтожает исходные элементы, рассматриваемые как мультимножество, что намного легче доказать. Если посмотреть с другой стороны, можно использовать формальную проверку, чтобы уменьшить накладные расходы на проверку времени выполнения, как уже упоминалось выше для статического анализа вместо формальной проверки. Действительно, можно начать с полностью проверенной, но, вероятно, медленной программы. Затем можно использовать формальную проверку (или статический анализ) для разгрузки мониторов, точно так же, как компилятор использует статический анализ для выполнения проверок корректности типа или безопасность памяти.

Увеличение охвата

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

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