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

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

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

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

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

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

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

Базовые подходы

Обзор процесса проверки на основе монитора, описанный Фальконе, Хавелундом и Регером в книге «Учебник по проверке во время выполнения»

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

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

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

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

Примеры

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

ИмеетСледующий

Свойство HasNext

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

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

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

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

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

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

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

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

SafeLock

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

∀ Поток t , Блокировка l : S →ε | S begin( t ) S end( t ) | S l .acquire( t ) S l .release( t )

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

Шаблон определяет сбалансированные последовательности вложенных пар begin/end и acquire/release для каждого Thread и Lock ( — пустая последовательность). Здесь begin и end ссылаются на начало и конец каждого метода в программе (за исключением вызовов acquire и release самих себя). Они параметричны в Thread, потому что необходимо связать начало и конец методов, если и только если они принадлежат одному Thread. События acquire и release также параметричны в Thread по той же причине. Они, кроме того, параметричны в Lock, потому что мы не хотим связывать освобождения одного Lock с приобретениями другого. В крайнем случае, возможно, что будет экземпляр свойства, т. е. копия механизма контекстно-свободного синтаксического анализа, для каждой возможной комбинации Thread с Lock; это происходит, опять же, интуитивно, потому что системы проверки во время выполнения могут реализовывать одну и ту же функциональность по-разному. Например, если в системе есть Threads , , и с Locks и , то возможно придется поддерживать экземпляры свойств для пар < , >, < , >, < , >, < , >, < , > и < , >. Это свойство следует отслеживать на предмет несоответствий шаблону, поскольку шаблон определяет правильное поведение. На рисунке справа показана трассировка, которая создает два нарушения этого свойства. Шаги вниз на рисунке представляют начало метода, а шаги вверх — конец. Серые стрелки на рисунке показывают соответствие между заданными захватами и освобождениями одного и того же Lock. Для простоты трассировка показывает только один Thread и один Lock. ${\displaystyle \epsilon }$ ${\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(), который возвращает true (видимый на графике потока управления).
• Эффективная генерация и управление мониторами . При мониторинге параметрических свойств, подобных приведенным в примерах выше, система мониторинга должна отслеживать состояние контролируемого свойства по отношению к каждому экземпляру параметра. Количество таких экземпляров теоретически не ограничено и на практике имеет тенденцию быть огромным. Важной исследовательской задачей является то, как эффективно отправлять наблюдаемые события именно тем экземплярам, ​​которые в них нуждаются. Связанная с этим задача заключается в том, как сохранить количество таких экземпляров небольшим (чтобы диспетчеризация была быстрее), или, другими словами, как избегать создания ненужных экземпляров как можно дольше и, в свою очередь, как удалять уже созданные экземпляры, как только они становятся ненужными. Наконец, алгоритмы параметрического мониторинга обычно обобщают аналогичные алгоритмы для генерации непараметрических мониторов. Таким образом, качество сгенерированных непараметрических мониторов диктует качество результирующих параметрических мониторов. Однако, в отличие от других подходов к проверке (например, проверки модели), количество состояний или размер сгенерированного монитора менее важны при проверке во время выполнения; на самом деле, некоторые мониторы могут иметь бесконечно много состояний, например, для свойства SafeLock выше, хотя в любой момент времени может произойти только конечное число состояний. Важно то, насколько эффективно монитор переходит из состояния в следующее состояние, когда он получает событие от исполняющей системы.

Указание свойств

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

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

Модели исполнения и предиктивный анализ

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

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

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

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

Связанная работа

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

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

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

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

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

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

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

Смотрите также

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

Ссылки

1. Эцио Барточчи и Илиес Фальконе (редакторы), Лекции по верификации времени выполнения — вводные и продвинутые темы, часть серии книг Lecture Notes in Computer Science (LNCS, том 10457), также часть подсерии книг Programming and Software Engineering (LNPSE, том 10457), 2018. Lecture Notes in Computer Science. Том 10457. 2018. doi :10.1007/978-3-319-75632-5. ISBN 978-3-319-75631-8. S2CID  23246713.
2. "RV'01 - Первый семинар по верификации времени выполнения". Конференции по верификации времени выполнения . 23 июля 2001 г. Получено 25 февраля 2017 г.
3. Клаус Хавелунд и Григоре Росу. 2004. Обзор инструмента проверки времени выполнения Java PathExplorer. Формальные методы в проектировании систем, 24(2), март 2004 г.
4. Стефан Сэвидж, Майкл Берроуз, Грег Нельсон, Патрик Собальварро и Томас Андерсон. 1997. Eraser: динамический детектор гонки данных для многопоточных программ. ACM Trans. Comput. Syst. 15(4), ноябрь 1997 г., стр. 391-411.
5. Мунджу Ким, Махеш Вишванатан, Инсуп Ли, Ханен Бен-Абделла, Сампат Каннан и Олег Сокольский, Формально заданный мониторинг временных свойств, Труды Европейской конференции по системам реального времени, июнь 1999 г.
6. Инсуп Ли, Сампат Каннан, Мунджу Ким, Олег Сокольский, Махеш Вишванатхан, «Гарантия выполнения на основе формальных спецификаций», Труды Международной конференции по методам и приложениям параллельной и распределенной обработки, июнь 1999 г.
7. Клаус Хавелунд, Использование анализа времени выполнения для руководства проверкой моделей программ Java, 7-й международный семинар SPIN, август 2000 г.
8. Клаус Хавелунд и Григоре Росу, Мониторинг программ с использованием переписывания, Автоматизированная разработка программного обеспечения (ASE'01), ноябрь 2001 г.
9. Yliès Falcone, Klaus Havelund и Giles, Учебное пособие по проверке времени выполнения, 2013