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

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

История и контекст [ править ]

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

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

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

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

Основные подходы [ править ]

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

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

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

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

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

Примеры [ править ]

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

HasNext [ править ]

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

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

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

UnsafeEnum [ править ]

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

Этот шаблон является параметрическим как в перечислении, так и в векторе. Интуитивно и, как указано выше, системы проверки времени выполнения не должны реализовывать свои параметрические мониторы таким образом, можно думать о параметрическом мониторе для этого свойства как о создании и отслеживании экземпляра непараметрического монитора для каждой возможной пары вектора и перечисления. Некоторые события могут касаться нескольких мониторов одновременно, например: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()возвращающий истину (видимый на графе потока управления).
• Эффективное создание мониторов и управление ими. При мониторинге параметрических свойств, подобных приведенным в примерах выше, системе мониторинга необходимо отслеживать состояние отслеживаемого свойства по отношению к каждому экземпляру параметра. Количество таких случаев теоретически неограниченно и на практике имеет тенденцию быть огромным. Важная исследовательская проблема заключается в том, как эффективно направлять наблюдаемые события именно тем экземплярам, ​​которые в них нуждаются. Связанная с этим проблема заключается в том, как сохранить небольшое количество таких экземпляров (чтобы ускорить отправку), или, другими словами, как избежать создания ненужных экземпляров как можно дольше и, вдвойне, как удалить уже созданные экземпляры, как только они становятся ненужными. Наконец, алгоритмы параметрического мониторинга обычно обобщают аналогичные алгоритмы для создания непараметрических мониторов. Таким образом,качество созданных непараметрических мониторов определяет качество результирующих параметрических мониторов. Однако, в отличие от других подходов к верификации (например, проверка модели), количество состояний или размер сгенерированного монитора менее важны при верификации во время выполнения; на самом деле, у некоторых мониторов может быть бесконечно много состояний, например, дляSafeLock выше, хотя в любой момент времени могло произойти только конечное число состояний. Важно то, насколько эффективно монитор переходит из состояния в следующее состояние, когда он получает событие от исполняющей системы.

Указание свойств [ править ]

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

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

Модели исполнения и прогнозный анализ [ править ]

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

Модификация поведения [ править ]

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

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

Связанные работы [ править ]

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

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

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

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

Увеличение охвата [ править ]

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

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

См. Также [ править ]

• Динамический анализ программы
• Профилирование (компьютерное программирование)
• Обнаружение ошибок во время выполнения
• Самозащита рабочего приложения (RASP)

Ссылки [ править ]