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

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

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

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

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

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

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

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

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

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

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

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

Примеры

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

HasNext

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

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

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

UnsafeEnum

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

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

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

Сафелок

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

∀ Нить t , Замок l : S →ε | S начало( т ) S конец( т ) | S l .acquire( t ) S l .release( t )

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

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

Задачи и приложения исследований

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

См. также

Ссылки

^ Эцио Барточчи и Юлиес Фальконе (редакторы), «Лекции по проверке времени выполнения — вводные и дополнительные темы», часть серии книг «Конспекты лекций по информатике» (LNCS, том 10457), а также часть подсерии книг «Программирование и программная инженерия» (LNPSE, том 10457), 2018 . Конспекты лекций по информатике. Том. 10457. 2018. doi : 10.1007/978-3-319-75632-5 . ISBN 978-3-319-75631-8 . S2CID 23246713 .
^ «RV'01 — Первый семинар по проверке времени выполнения» . Конференции по проверке работоспособности . 23 июля 2001 года . Проверено 25 февраля 2017 г.
^ Клаус Хавелунд и Григоре Рошу. 2004. Обзор средства проверки времени выполнения Java PathExplorer. Формальные методы проектирования систем, 24 (2), март 2004 г.
^ Стефан Сэвидж, Майкл Берроуз, Грег Нельсон, Патрик Собальварро и Томас Андерсон. 1997. Eraser: детектор динамической гонки данных для многопоточных программ. АКМ Транс. Вычислить. Сист. 15(4), ноябрь 1997 г., стр. 391–411.
↑ Мунджу Ким, Махеш Вишванатан, Инсуп Ли, Ханен Бен-Абделла, Сампат Каннан и Олег Сокольский, Формально заданный мониторинг временных свойств, Материалы Европейской конференции по системам реального времени, июнь 1999 г.
^ Инсуп Ли, Сампат Каннан, Мунджу Ким, Олег Сокольский, Махеш Вишванатан, Обеспечение выполнения на основе формальных спецификаций, материалы международной конференции по методам и приложениям параллельной и распределенной обработки, июнь 1999 г.
^ Клаус Хавелунд, Использование анализа времени выполнения для проверки моделей программ на Java, 7-й международный семинар SPIN, август 2000 г.
^ Клаус Хавелунд и Григоре Росу, Программы мониторинга с использованием переписывания, автоматизированная разработка программного обеспечения (ASE'01), ноябрь 2001 г.
^ Перейти обратно: ^а ^б Юлиес Фальконе, Клаус Хавелунд и Джайлс, Учебное пособие по проверке времени выполнения, 2013 г.

[1] Эцио Барточчи и Юлиес Фальконе (редакторы), «Лекции по проверке времени выполнения — вводные и дополнительные темы», часть серии книг «Конспекты лекций по информатике» (LNCS, том 10457), а также часть подсерии книг «Программирование и программная инженерия» (LNPSE, том 10457), 2018 . Конспекты лекций по информатике. Том. 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 г.

[Havelund2001Overview-3] Клаус Хавелунд и Григоре Рошу. 2004. Обзор средства проверки времени выполнения Java PathExplorer. Формальные методы проектирования систем, 24 (2), март 2004 г.

[SavageTCS1997-4] Стефан Сэвидж, Майкл Берроуз, Грег Нельсон, Патрик Собальварро и Томас Андерсон. 1997. Eraser: детектор динамической гонки данных для многопоточных программ. АКМ Транс. Вычислить. Сист. 15(4), ноябрь 1997 г., стр. 391–411.

[5] Мунджу Ким, Махеш Вишванатан, Инсуп Ли, Ханен Бен-Абделла, Сампат Каннан и Олег Сокольский, Формально заданный мониторинг временных свойств, Материалы Европейской конференции по системам реального времени, июнь 1999 г.

[6] Инсуп Ли, Сампат Каннан, Мунджу Ким, Олег Сокольский, Махеш Вишванатан, Обеспечение выполнения на основе формальных спецификаций, материалы международной конференции по методам и приложениям параллельной и распределенной обработки, июнь 1999 г.

[HavelundSPIN2000-7] Клаус Хавелунд, Использование анализа времени выполнения для проверки моделей программ на Java, 7-й международный семинар SPIN, август 2000 г.

[HavelundRosuASE2001-8] Клаус Хавелунд и Григоре Росу, Программы мониторинга с использованием переписывания, автоматизированная разработка программного обеспечения (ASE'01), ноябрь 2001 г.

[havelundRVTutorial2012-9] Перейти обратно: ^а ^б Юлиес Фальконе, Клаус Хавелунд и Джайлс, Учебное пособие по проверке времени выполнения, 2013 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]