Алгоритмы ускорения планирования траекторий выполнения программ при направленном тестировании тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат наук Щербаков Андрей Сергеевич

• Щербаков Андрей Сергеевич
• кандидат наук
• 2021

Оглавление диссертации кандидат наук Щербаков Андрей Сергеевич

Введение

Глава 1. Обзор основных подходов к динамической верификации

программного обеспечения

1.1 Основные представления и логики, используемой при моделировании свойств программ

1.2 Методы, использующие абстракцию модели

1.3 Индуктивные методы доказательства свойств

1.3.1 Базовые подходы к индуктивному доказательству

1.3.2 к-индукция

1.3.3 Подходы к улучшению генерализации выражений

1.3.4 ГС3

1.3.5 Расширения методов абстрактной индукции

1.3.6 Адаптация индуктивных методов

к моделированию программ

1.4 Направленное тестирование

1.4.1 Вариации применения направленного тестирования

1.5 Выводы по главе 1 и постановка задачи

Глава 2. Методы ускорения направленного тестирования,

использующие ограничение повторных обходов ветвей кода

2.1 Введение в принцип ограничения реальтернаций

2.2 Базовые эксперименты с ограничением реальтернаций

2.2.1 Сопоставление с ранним исследованием

2.3 Влияние циклов в программе на эффективность метода

2.4 Учет контекста вызовов

2.5 Ослабление ограничения реальтернаций на основе анализа зависимостей данных

2.5.1 Представление информации о траекториях

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

2.5.2 Описание алгоритма учёта зависимостей

Стр.

2.5.3 Результаты применения алгоритма

2.5.4 Выводы по главе

Глава 3. Быстрый алгоритм нахождения доступных вершин графа

управления при ограничениях траекторий

3.1 Введение в задачу

3.2 Альтернативная постановка задачи. Функции доступности D и

3.3 Предварительные замечания по вычислению D

3.4 Репрезентативные структуры

3.5 Использование остовных деревьев для оптимизации вычисления £

3.6 Вычисление интервалов вершин в архитектуре планирования тестов

3.7 Использование «запасных» двоичных деревьев

3.8 Выравнивание двоичных деревьев

3.9 Вычисление множеств «внешних» узлов

3.10 Обработка вызовов функций

3.11 Замечания по интеграции алгоритма

3.12 Моделирование

3.12.1 Разборщик (Parser)

3.12.2 Преобразователь интерфейса исключений

3.12.3 Вычисление £ в графе

3.13 Эксперименты

3.13.1 Эффективность поиска

3.13.2 Сравнение типов очередей

3.13.3 Сравнение эффективности контейнеров (куч)

3.14 Выводы по главе

Глава 4. Алгоритмы реконструкции графа управления на основе

трасс событий

4.1 Алгоритм построения автомата

4.1.1 Мотивация

4.1.2 Введение в алгоритм построения автомата

4.1.3 Архитектура

4.2 Результаты тестирования алгоритма

Стр.

4.3 Использование регулярных выражений для обобщения

последовательностей

4.3.1 Представление исходного ациклического графа для построения регулярных выражений

4.3.2 Алгоритм ветвящегося выравнивания

4.3.3 Поиск повторов

4.3.4 Выводы по главе

Список сокращений и условных обозначений

Словарь терминов

Список литературы

Список рисунков

Список таблиц

Введение диссертации (часть автореферата) на тему «Алгоритмы ускорения планирования траекторий выполнения программ при направленном тестировании»

Введение

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

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

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

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

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

Использование моделей, учитывающей зависимости условий переходов через присвоения переменных, при этом оказывается сложным из-за недостаточной разработанности соответствующих алгоритмов и эвристик. Из-за возникающей в общем случае необходимости перебора различных комбинаций направлений переходов требуемое для достижения заданной полноты тестирования количество единичных тестов оказывается экспоненциальным относительно размера программы. Это исключает полноценное применение направленного тестирования для большинства разрабатываемых программ. Чтобы сделать возможным использование современных методов моделирования дискретных систем в направленном тестирования ПО, данный недостаток должен быть устранён.

Направленное тестирование фактически одновременно преследует две взаимоисключающие цели: с одной стороны, обеспечить максимальное покрытие

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

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

Особую трудность представляет учет зависимостей через присваивания значений в динамически выделяемых областях памяти, так как:

- из-за разнообразия способов прямой и непрямой адресации переменной или элемента структуры (массива) установить соответствие операций чтения данных операциям их записи возможно далеко не всегда;

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

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

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

В диссертационном исследовании рассматриваются следующие основные вопросы:

- Исследование возможности повышения скорости тестирования с применением эвристических подходов, основанных на ограничении полного количества отклонений направлений переходов управления от направлений, наблюдаемых в некотором наборе базовых траекторий

- Разработка простого универсального способа формулирования условий для планирования траекторий выполнения с учетом обнаруженных зависимостей через присвоения значений данных.

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

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

Степень разработанности темы. Теоретические изыскания в области обеспечения качества программ появились практически одновременно с самими компьютерными программами. Ранние исследования Ч. Хоара [82] и УКрейга [45; 47] в области математической логики во многом определили современное состояние моделирования и верификации цифровых систем, сделали возможным применение индуктивных методов доказательства свойств. Однако широкое развитие верификации программ как технической дисциплины, ориентированной в большей степени на оптимизацию потребления вычислительных ресурсов, происходило намного позднее, уже в 2000-е годы. В этой связи можно упомянуть работы зарубежных авторов, таких как Д. Бейер [53; 54; 72; 77—81; 116],

A. Брэдли [89; 91—94; 99; 101], Годефройд [120; 132; 133], Д. Кронинг [49; 69; 135], К. Макмиллан [37; 48; 50; 86; 112], Ф. Соменци [95; 99; 100; 107], А. Ци-матти [102; 105; 109; 110; 114; 116], и отечественные исследования Б.М. Баска [126], В.С. Буренкова [18—20], А.Г. Зыкова [125; 147; 150—152; 154; 163; 165],

B.В. Липаева [121], А.С. Камкина [131; 157; 170; 171], О.Ф. Немолочнова [147; 150—154; 163; 164] и других. Несмотря на впечатляющий прогресс, достигнутый в моделировании свойств цифровых систем, можно отметить существенный общий недостаток предлагаемых в литературе подходов к верификации ПО, заключающийся в отсутствии внимания к анализу возможности развития определённых ситуаций в программе в зависимости от выбранного пути её выполнения. По-видимому, это исторически обусловлено тем, что подходы к верификации

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

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

Для достижения поставленной цели необходимо было решить следующие задачи:

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

2. Исследовать возможность учёта неточной информации о зависимостях по данным в указанных стратегиях.

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

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

5. Разработать и исследовать алгоритмы аппроксимации графа управления на основе наблюдаемых путей выполнения тестов.

Научная новизна:

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

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

3. Разработан и экспериментально подтверждён алгоритм быстрого вычисления дополнения множеств доступных вершин в графе управления при

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

4. Предложены алгоритмы построения аппроксимации графа на основе набора примеров путей в нём с помощью минимизации расстояния редактирования между примером и графом.

Практическая значимость. Предложенные решения легко интегрируются в системы направленного тестирования программ и аппаратно-программных комплексов, при этом время тестирования снижается в 6 и более раз без ухудшения покрытия ветвей тестируемой программы. Результаты исследований были использованы при разработке внутренних средств тестирования компании Intel.

Методология и методы исследования. В диссертационном исследовании преимущественно применялись экспериментально-аналитический и экспериментальный методы исследования гипотез.

Основные положения, выносимые на защиту:

1. Метод оптимизации числа тестов путём ограничения количества изменяемых направлений условных переходов в траекториях выполнения программ при их направленном тестировании.

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

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

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

Достоверность полученных результатов обеспечивается исследованиями эффективности предложенных методов непосредственным измерением ряда статистических величин в экспериментах. Эксперименты проводились с репрезентативной выборкой из более 100 практических приложений, в основном, из числа общедоступных проектов с открытым кодом.

Апробация работы. Основные результаты работы докладывались на всероссийских научно-технических конференциях "Проблемы разработки перспективных микро- и наноэлектронных систем" (МЭС) 2012, 2014, 2016, 2018 гг., пятой международной конференции «Анализ изображений, социальных сетей

и текстов» (AIST 2016), конференции "The 17th Annual Workshop of the Australasian Language Technology Association" (2019).

Личный вклад. Автору принадлежит:

1. выделение исследуемых направлений оптимизации тестирования и формулирование соответствующих им критериев целесообразности отдельных тестов;

2. разработка предложенных в диссертационной работе алгоритмов:

- алгоритма ограничения реальтернаций условных переходов при направленном тестировании (варианты: без учета зависимостей по данным и с учётом таких зависимостей);

- алгоритма быстрого вычисления функций доступности узлов в графе управления;

- алгоритмов реконструкции графа управления из наблюдаемых трасс выполнения тестов (в произвольном виде и в виде автомата для регулярного выражения)

3. разработка методик и проведение экспериментальных подтверждений;

4. создание программных приложений, реализующих предложенные алгоритмы;

5. выработка рекомендаций по применимости и выбору параметров алгоритмов и эвристик.

В работе, выполненной в соавторстве, вклад автора составляет 50%.

Публикации. Основные результаты по теме диссертации изложены в 6 печатных изданиях, 4 из которых изданы в журналах, рекомендованных ВАК, 1 — в периодических научных журналах, индексируемых Web of Science и Scopus, 1 — в тезисах докладов [1—6].

Объем и структура работы. Диссертация состоит из введения, четырёх глав и заключения. Полный объём диссертации составляет 206 страниц, включая 40 рисунков и 5 таблиц. Список литературы содержит 214 наименований.

Глава 1. Обзор основных подходов к динамической верификации

программного обеспечения

1.1 Основные представления и логики, используемой при моделировании

свойств программ

Прежде, чем перейти к обзору существующих методов и алгоритмов верификации сценариев работы ПО, необходимо рассмотреть основные типы логик и структур, применяемых для описания спецификаций свойств и анализа поведения модели с точки зрения их выполнения. В основе интерпретации состояний системы, как правило, лежит логика первого порядка, или исчисление предикатов. Такая логика является формальным исчислением, допускающим выражения, аргументами которых являются переменные, предикаты и функции от выражений. Множество функций состоит из двух подмножеств — функций и предикатов. Также в выражениях используются переменные, логические операции (главным образом отрицание, дизъюнкция, конъюнкция и импликация), кванторы (всеобщности — V и существования — 3), символы пунктуации (скобки, запятая) и, возможно, дополнительные символы, обусловленные спецификой области определения. Логика первого порядка позволяет описывать состояние цифровой системы в произвольном удобном базисе переменных, например, в базисе входных значений или внутренних состояний программы.

Однако для описания последовательностей состояний системы, сложных правил перехода и свойств, включающих в свое выражение множество допустимых состояний в разные моменты времени, необходимо расширение выразительных средств. В таком случае обычно применяются автоматы или подобные им решения. Автоматом называется набор А = (Б,Х,У,6,Л), где Б — множество состояний автомата; X, У — множества (алфавиты) возможных состояний (букв) на его входе и на выходе; 5 : X х Б ^ Б - функция переходов, ставящая в соответствие состояние автомата в следующий момент времени комбинации текущего состояния автомата и состояния его входа; Л : X х Б ^ У - функция выхода (аналогично, для состояния выхода в следующий момент). В практике компьютерного моделирования и верификации используется конечные автоматы, то есть автоматы с конечным множеством состояний Б.

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

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

- абстрактное представление состояний модели через состояния автомата;

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

Существуют простые алгоритмы приведения недетерминированого автомата (НДА) к детерминированному (ДА) на основе теоремы о детерминизации [7], однако в результате такого преобразования возможен экспоненциальный взрыв числа состояний.

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

Заметим, что автомат сам по себе недостаточно выразителен для описания реальных цифровых систем. Главным образом это связано с повсеместным использованием числовых данных. Каждой возможной совокупности значений

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

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

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

- Состояния соответствуют логическим функциям над предикатами из заранее определенного набора;

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

2Конечно, размер реальной доступной памяти в программе всегда ограничен каким-либо пределом. Однако построение конечного автомата для всех возможных состояний в рамках максимального доступного числа битов памяти выходит далеко за пределы возможностей вычислительных средств.

следующих во времени состояний. Каждое состояние имеет хотя бы одно следующее состояние (возможно, само себя).

Структура Крипке недетерминистична, поэтому ее возможно построить для параллельных и волатильных программ. Обычно такая структура, как и автомат, наглядно представляется в виде графа, где состояния играют роль вершин, а возможные переходы - рёбер. В отличие от автомата, метки на рёбрах графа структуры Крипке отсутствуют, так как возможность перехода в данное состояние однозначно определяется предыдущим. Используются и схожие логические модели, в которых логическими выражениями помечены не вершины, а рёбра, например, LTS (Labelled Transition System).

Для работы с высказываниями, истинность которых может изменяться с течением времени, были разработаны темпоральные логики, являющиеся вариантами модальной логики. Наиболее распространены два основных типа темпоральной логики: логика ветвящегося времени — CTL (concurrent time logic) и логика линейного времени - LTL (linear time logic). Помимо логических операторов (заметим, что в нашем случае под логическим операторами мы подразумеваем все операторы логики первого порядка), в темпоральных логиках вводятся модальные операторы, связанные с последовательностью событий во времени (Таблица 1).

Таблица 1 — Список темпоральных операторов

Символ Операция Описание

x U y Until х верно с текущего момента до тех пор, пока впервые не возникнет истинное значение у

X x Next х верно в следующий момент

G x Globally х верно во все моменты начиная с данного

F x Future х верно в данный или какой-либо последующий момент

A x All (V) х верно независимо от рассматриваемого сценария

E x Exists (3) х верно при каком-либо из возможных сценариев

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

объединяет выразительные возможности CTL и LTL. В ней возможны любые комбинации кванторов и темпоральных операторов. Вариантом CTL, ориентированным на использование с моделями, представленными событиями, является ACTL - Action based Computational Tree Logic.

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

Список литературы диссертационного исследования кандидат наук Щербаков Андрей Сергеевич, 2021 год

Список литературы

1. Щербаков, А. Ускорение направленного автоматического тестирования ПО в практике моделирования СБИС за счет сокращения обходов ветвей условных переходов [Текст] / А. Щербаков // Проблемы разработки перспективных микро-и наноэлектронных систем (МЭС). — 2012. — № 1. — С. 89—94.

2. Щербаков, А. Ускорение направленного тестирования встроенного и внешнего ПО СБИС путем учета потока данных при ограничении вариативности траекторий выполнения [Текст] / А. Щербаков // Проблемы разработки перспективных микро-и наноэлектронных систем (МЭС). — 2014. — № 2. — С. 15-20.

3. Щербаков, А. Быстрый алгоритм нахождения доступных вершин графа управления при ограничениях траекторий [Текст] / А. Щербаков // Проблемы разработки перспективных микро-и наноэлектронных систем (МЭС). — 2018. — № 2. -С. 92-98.

4. Щербаков, А. Быстрый алгоритм учета зависимостей данных при анализе и тестировании программного обеспечения СБИС [Текст] / А. Щербаков // Проблемы разработки перспективных микро-и наноэлектронных систем (МЭС). - 2016. - № 2. - С. 76-83.

5. Shcherbakov, A. A Branching Alignment-Based Synthesis of Regular Expressions. [Текст] / A. Shcherbakov // AIST (Supplement). — 2016. — С. 315-328.

6. Shcherbakov, A. A string-to-graph constructive alignment algorithm for discrete and probabilistic language modeling [Текст] / A. Shcherbakov, E. Vylomova // Proceedings of the The 17th Annual Workshop of the Australasian Language Technology Association. — 2019. — С. 186—191.

7. Дискретная математика [Текст] / А. И. Белоусов [и др.]. — 2006.

8. Клини, С. К. Математическая логика [Текст] / С. К. Клини. — Мир, 1973.

9. Логика вопросов и ответов [Текст] / Н. Белнап [и др.]. — Прогресс, 1981.

10. Multi-valued symbolic model-checking [Текст] / M. Chechik [и др.] // ACM Transactions on Software Engineering and Methodology (TOSEM). — 2003. — Т. 12, № 4. — С. 371-408.

11. Зайцев, Д. Логическое следование и выделенные значения [Текст] / Д. Зайцев,Я. Шрамко// Логические исследования. —2004. —№ 11. — С. 126—137.

12. Graf, S. Construction of abstract state graphs with PVS [Текст] / S. Graf, H. Sa'idi // International Conference on Computer Aided Verification. — Springer. 1997. — С. 72-83.

13. Colón, M. A. Generating finite-state abstractions of reactive systems using decision procedures [Текст] / M. A. Colón, T. E. Uribe // International Conference on Computer Aided Verification. — Springer. 1998. — С. 293—304.

14. Roorda, J.-W SAT-based assistance in abstraction refinement for symbolic trajectory evaluation [Текст] / J.-W. Roorda, K. Claessen // International Conference on Computer Aided Verification. — Springer. 2006. — С. 175—189.

15. Modular verification of software components in C [Текст] / S. Chaki [и др.] // IEEE Transactions on Software Engineering. — 2004. — Т. 30, № 6. — С. 388-402.

16. Dill, D. Мш-ф Description Language and Verifier [Текст] / D. Dill, C. Ip, U. Stern// Available on: http://verify. standford. edu/dill/murphi. html. — 1996.

17. De Nicola, R. Three logics for branching bisimulation [Текст] / R. De Nicola, F. Vaandrager // Journal of the ACM (JACM). - 1995. - Т. 42, № 2. -С. 458-487.

18. Буренков, В. Анализ применимости формальных методов к верификации протоколов когерен тности кэш-памяти масштабируемых систем [Текст] / В. Буренков // Вопросы радиоэлектроники. — 2015. — № 1. — С. 105—116.

19. Буренков, В. Метод масштабируемой верификации PROMELA-моделей протоколов когерентнос ти кэш-памяти [Текст] / В. Буренков, А. Камкин // Проблемы разработки перспективных микро-и наноэлектронных систем (МЭС ). - 2016. - № 2. - С. 54-60.

20. Буренков, В. С. О консервативном преобразовании формальных моделей, используемых примени тельно к масштабируемым системам для верификации протоколов когерентности памяти [Текст] / В. С. Буренков // Вопросы радиоэлектроники. — 2016. — № 3. — С. 48—52.

21. Peleska, J. A unified approach to abstract interpretation, formal verification and testing of C/C++ modules [Текст] / J. Peleska // International Colloquium on Theoretical Aspects of Computing. — Springer. 2008. — С. 3—22.

22. Havelund, Z. Model checking java programs using java pathfinder [Текст] / K. Havelund, T. Pressburger // International Journal on Software Tools for Technology Transfer. — 2000. — Т. 2, № 4. — С. 366—381.

23. Pâsâreanu, C. S. Finding feasible counter-examples when model checking abstracted Java programs [Текст] / C. S. Pâsâreanu, M. B. Dwyer, W. Visser // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2001. — С. 284—298.

24. Huch, F. Verification of Erlang programs using abstract interpretation and model checking [Текст]. Т. 34 / F. Huch. — ACM, 1999.

25. Blanc, ^.Verifying C++ with STL containers via predicate abstraction [Текст] / N. Blanc, A. Groce, D. Kroening // Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering. —ACM. 2007. — С. 521-524.

26. Abrial, J.-R. Using design patterns in formal methods: An Event-B approach [Текст] / J.-R. Abrial, T. S. Hoang // International Colloquium on Theoretical Aspects of Computing. — Springer. 2008. — С. 1—2.

27. CPP2XMI: reverse engineering of UML class, sequence, and activity diagrams from C++ source code [Текст] / E. Korshunova [и др.] // 2006 13th Working Conference on Reverse Engineering. — IEEE. 2006. — С. 297—298.

28. Peleska, J. Integrated and automated abstract interpretation, verification and testing of c/c++ modules [Текст] / J. Peleska // Concurrency, Compositionality, and Correctness. — Springer, 2010. — С. 277—299.

29. Jensen, T. Verification of control flow based security properties [Текст] / T. Jensen, D. Le Métayer, T. Thorn // Security and privacy, 1999. Proceedings of the 1999 IEEE symposium on. — IEEE. 1999. — С. 89—103.

30. Static analysis and verification of aerospace software by abstract interpretation [Текст] / J. Bertrane [и др.] // AIAA Infotech@ Aerospace. — 2010. — № 2010-3385. — С. 1-38.

31. Formal verification of critical aerospace software [Текст] / V. Wiels [и др.] // AerospaceLab. — 2012. — № 4. — p—1.

32. Counterexample-guided abstraction refinement [Текст] / E. Clarke [и др.] // International Conference on Computer Aided Verification. — Springer. 2000. — С. 154-169.

33. Clarke, E. M. Model checking and abstraction [Текст] / E. M. Clarke, O. Grumberg, D. E. Long // ACM transactions on Programming Languages and Systems (TOPLAS). - 1994. - Т. 16, № 5. - С. 1512-1542.

34. Kurshan, R. P. Computer-aided verification of coordinating processes: the automata-theoretic approach [Текст] / R. P. Kurshan. — Princeton university press, 1994.

35. Lee, K. Dynamic model abstraction [Текст] / K. Lee, P. A. Fishwick // Proceedings of the 28th conference on Winter simulation. — IEEE Computer Society. 1996. - С. 764-771.

36. Pardo, A. Incremental CTL model checking using BDD subsetting [Текст] / A. Pardo, G. D. Hachtel // Proceedings of the 35th annual Design Automation Conference. — ACM. 1998. — С. 457—462.

37. McMillan, K. L. Verification of infinite state systems by compositional model checking [Текст] / K. L. McMillan // Advanced Research Working Conference on Correct Hardware Design and Verification Methods. -- Springer. 1999. -С. 219-237.

38. Bruns, G. Model checking partial state spaces with 3-valued temporal logics [Текст] / G. Bruns, P. Godefroid // International Conference on Computer Aided Verification. — Springer. 1999. — С. 274—287.

39. Benedikt, M. A decidable logic for linked data structures [Текст] / M. Benedikt, T. Reps, M. Sagiv // Proc. 8th ESOP. Т. 6. - 1999. - С. 7.

40. Cousot, P. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints [Текст] / P. Cousot, R. Cousot // Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. —ACM. 1977. — С. 238—252.

41. Dams, D. Abstract interpretation of reactive systems [Текст] / D. Dams, R. Gerth, O. Grumberg // ACM Transactions on Programming Languages and Systems (TOPLAS). - 1997. - Т. 19, № 2. - С. 253-291.

42. Ball, T. Boolean and Cartesian abstraction for model checking C programs [Текст] / T. Ball, A. Podelski, S. K. Rajamani // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2001. —С. 268-283.

43. Clarke, E. M. Automatic verification of finite-state concurrent systems using temporal logic specifications [Текст] /E. M. Clarke, E. A. Emerson, A. P. Sistla // ACM Transactions on Programming Languages and Systems (TOPLAS). — 1986. - Т. 8, № 2. - С. 244-263.

44. Lazy abstraction [Текст] / T. A. Henzinger [и др.] // ACM SIGPLANNotices. — 2002. — Т. 37, № 1. — С. 58—70.

45. Craig, W. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory [Текст] / W. Craig // The Journal of Symbolic Logic. — 1957. — Т. 22, № 03. - С. 269-285.

46. Albarghouthi, A. Craig interpretation [Текст] / A. Albarghouthi, A. Gurfinkel, M. Chechik // International Static Analysis Symposium. — Springer. 2012. — С. 300-316.

47. Craig, W. Linear reasoning. A new form of the Herbrand-Gentzen theorem [Текст] / W. Craig // The Journal of Symbolic Logic. — 1957. — Т. 22, № 03. — С. 250-268.

48. McMillan, K. L. Lazy abstraction with interpolants [Текст] / K. L. McMillan // International Conference on Computer Aided Verification. — Springer. 2006. — С. 123-136.

49. Kroening, D. Interpolation-based software verification with WOLVERINE [Текст] / D. Kroening, G. Weissenbacher // International Conference on Computer Aided Verification. — Springer. 2011. — С. 573—578.

50. McMillan, K. L. Lazy annotation for program testing and verification [Текст] / K. L. McMillan // International Conference on Computer Aided Verification. — Springer. 2010. - С. 104-118.

51. Counterexample-guided abstraction refinement for symbolic model checking [Текст] / E. Clarke [и др.] // Journal of the ACM (JACM). — 2003. — Т. 50, № 5. — С. 752—794.

52. Gupta, A. Reconsidering CEGAR: Learning good abstractions without refinement [Текст] / A. Gupta, E. Clarke // 2005 International Conference on Computer Design. — IEEE. 2005. — С. 591—598.

53. Beyer, D. Explicit-state software model checking based on CEGAR and interpolation [Текст] / D. Beyer, S. Löwe // International Conference on Fundamental Approaches to Software Engineering. — Springer. 2013. —

C. 146-162.

54. Beyer, D. Program analysis with dynamic precision adjustment [Текст] /

D. Beyer, T. A. Henzinger, G. Theoduloz // Automated Software Engineering, 2008. ASE 2008. 23rd IEEE/ACM International Conference on. — IEEE. 2008. — С. 29-38.

55. Kobayashi, ^.Predicate abstraction and CEGAR for higher-order model checking [Текст] /N. Kobayashi, R. Sato, H. Unno //ACM SIGPLANNotices. Т. 46. - ACM. 2011. - С. 222-233.

56. Constrained monotonic abstraction: A cegar for parameterized verification [Текст] / P. A. Abdulla [и др.] // International Conference on Concurrency Theory. — Springer. 2010. — С. 86—101.

57. What's decidable about hybrid automata? [Текст] / T. A. Henzinger [и др.] // Proceedings of the twenty-seventh annual ACM symposium on Theory of computing. — ACM. 1995. — С. 373—382.

58. Hybrid automata-based cegar for rectangular hybrid systems [Текст] / P. Prabhakar [и др.] // Formal Methods in System Design. — 2015. — Т. 46, № 2. — С. 105-134.

59. Katoen, J.-P. A Markov reward model checker [Текст] / J.-P. Katoen, M. Khattri, I. Zapreevt // Second International Conference on the Quantitative Evaluation of Systems (QEST'05). - IEEE. 2005. - С. 243-244.

60. Kwiatkowska, M. Game-based abstraction for Markov decision processes [Текст] / M. Kwiatkowska, G. Norman, D. Parker // Third International Conference on the Quantitative Evaluation of Systems-(QEST'06). — IEEE. 2006. — С. 157-166.

61. Hermanns, H. Probabilistic cegar [Текст] / H. Hermanns, B. Wachter, L. Zhang // International Conference on Computer Aided Verification. — Springer. 2008. — С. 162-175.

62. Hansson, H. A logic for reasoning about time and reliability [Текст] / H. Hansson, B. Jonsson // Formal aspects of computing. — 1994. — Т. 6, №5. —С. 512—535.

63. PRISM: A tool for automatic verification of probabilistic systems [Текст] / A. Hinton [и др.] // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2006. — С. 441—444.

64. Highlevel verification of control intensive systems using predicate abstraction [Текст] / E. Clarke [и др.] // Formal methods and models for system design. — Springer, 2004. — С. 159—179.

65. Clarke, E. Predicate abstraction and refinement techniques for verifying Verilog [Текст] / E. Clarke, H. Jain, D. Kroening // DTIC Document. — 2004.

66. Predicate abstraction of ANSI-C programs using SAT [Текст] / E. Clarke [и др.] // Formal Methods in System Design. — 2004. — Т. 25, № 2/3. —

C. 105-127.

67. SATABS: SAT-based predicate abstraction for ANSI-C [Текст] / E. Clarke [и др.] // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2005. — С. 570—574.

68. Word level predicate abstraction and refinement for verifying RTL verilog [Текст] / H. Jain [и др.] // Proceedings of the 42nd annual Design Automation Conference. — ACM. 2005. — С. 445—450.

69. Kroening, D. Checking consistency of C and Verilog using predicate abstraction and induction [Текст] / D. Kroening, E. Clarke // Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design. — IEEE Computer Society. 2004. — С. 66—72.

70. Abstractions from proofs [Текст] / T. A. Henzinger [и др.] // ACM SIGPLAN Notices. Т. 39. - ACM. 2004. - С. 232-244.

71. Clarke, E. Verification of SpecC using predicate abstraction [Текст] / E. Clarke, H. Jain, D. Kroening // Formal Methods in System Design. — 2007. — Т. 30, № 1. — С. 5-28.

72. Beyer, D. Predicate abstraction with adjustable-block encoding [Текст] /

D. Beyer, M. E. Keremoglu, P. Wendler // Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design. — FMCAD Inc. 2010. — С. 189-198.

73. Automatically refining abstract interpretations [Текст] / B. S. Gulavani [и др.] // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2008. — С. 443-458.

74. Шмелёв, В. Автономная верификация микропроцессоров на основе эталонных моделей разного уровня абстракции [Текст] / В. Шмелёв, И. Стотланд // В сб.: Научные труды Всероссийской научно-технической конференции «Проблемы разработки перспективных микро-и наноэлектронных систем (МЭС). Т. 1. — 2012. - С. 435-440.

75. Лебедев, Д. Автономная верификация контроллеров сопряжения интерфейсов на основе эталонных функциональных моделей [Текст] / Д. Лебедев, И. Стотланд // Вопросы радиоэлектроники. — 2018. — № 2. — С. 81—86.

76. Петроченков, М. В. Методика автономной верификации устройств подсистемы памяти многоядерны х микропроцессоров [Текст] / М. В. Петро-ченков, И. А. Стотланд // Вопросы радиоэлектроники. -- 2016. -- № 3. -С. 42--47.

77. Beyer, D. Configurable software verification: Concretizing the convergence of model checking and program analysis [Текст] / D. Beyer, T. A. Henzinger, G. Theoduloz // International Conference on Computer Aided Verification. — Springer. 2007. — С. 504—518.

78. Beyer, D. CPAchecker: A tool for configurable software verification [Текст] / D. Beyer, M. E. Keremoglu // International Conference on Computer Aided Verification. — Springer. 2011. — С. 184—190.

79. Beyer, D. Competition on software verification [Текст] / D. Beyer // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2012. — С. 504—524.

80. Beyer, D. Second competition on software verification [Текст] / D. Beyer // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2013. — С. 594—609.

81. Beyer, D. Software verification and verifiable witnesses [Текст] / D. Beyer // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2015. — С. 401—416.

82. Hoare, C. A. R. An axiomatic basis for computer programming [Текст] / C. A. R. Hoare // Communications of the ACM. — 1969. — Т. 12, № 10. — С. 576—580.

83. Floyd, R. W. Assigning meanings to programs [Текст] / R. W. Floyd // Mathematical aspects of computer science. — 1967. — Т. 19, № 19—32. — С. 1.

84. Clarke andE, E. A. Emerson. Synthesis of synchronization skeletons for branching time tem poral logic [Текст] / E. Clarke andE // L ogic o f Progra m s: W or k s h o p. Springer Verlag, May. — 1981. — Т. 1, № 9. — С. 81.

85. De Moura, L. Bounded model checking and induction: From refutation to verification [Текст] / L. De Moura, H. RueB, M. Sorea // International Conference on Computer Aided Verification. — Springer. 2003. — С. 14—26.

86. McMillan, K. L. Applying SAT methods in unbounded symbolic model checking [Текст] / K. L. McMillan // International Conference on Computer Aided Verification. — Springer. 2002. — С. 250—264.

87. De Moura, L. Lazy theorem proving for bounded model checking over infinite domains [Текст] / L. De Moura, H. RueB, M. Sorea // International Conference on Automated Deduction. — Springer. 2002. — С. 438—455.

88. Sheeran, M. Checking safety properties using induction and a SAT-solver [Текст] / M. Sheeran, S. Singh, G. Stalmarck // International conference on formal methods in computer-aided design. — Springer. 2000. — С. 127—144.

89. Bradley, A. R. Verification constraint problems with strengthening [Текст] / A. R. Bradley, Z. Manna // International Colloquium on Theoretical Aspects of Computing. — Springer. 2006. — С. 35—49.

90. Даффин, Р. Д. Геометрическое программирование [Текст] / Р. Д. Даффин, Э. Л. Питерсон, К. Зенер. — 2007.

91. Bradley, A. R. Checking safety by inductive generalization of counterexamples to induction [Текст] / A. R. Bradley, Z. Manna // Formal Methods in Computer Aided Design, 2007. FMCAD'07. — IEEE. 2007. — С. 173—180.

92. Bradley, A. R. Property-directed incremental invariant generation [Текст] / A. R. Bradley, Z. Manna // Formal Aspects of Computing. — 2008. — Т. 20, № 4/5. — С. 379—405.

93. Bradley, A. R. K-step relative inductive generalization [Текст] / A. R. Bradley // arXiv preprint arXiv:1003.3649. — 2010.

94. Bradley, A. R. SAT-based model checking without unrolling [Текст] / A. R. Bradley // International Workshop on Verification, Model Checking, and Abstract Interpretation. — Springer. 2011. — С. 70—87.

95. Somenzi, F. IC3: where monolithic and incremental meet. [Текст] / F. Somenzi, A. R. Bradley // FMCAD. Т. 2011. — 2011. — С. 3-8.

96. Een, N.Efficient implementation of property directed reachability [Текст] / N. Een, A. Mishchenko, R. Brayton // Formal Methods in Computer-Aided Design (FMCAD), 2011. — IEEE. 2011. — С. 125—134.

97. Dershowitz, N. A scalable algorithm for minimal unsatisfiable core extraction [Текст] / N. Dershowitz, Z. Hanna, A. Nadel // International Conference on Theory and Applications of Satisfiability Testing. — Springer. 2006. — С. 36—41.

98. Silva, J. P. M. GRASP—a new search algorithm for satisfiability [Текст] / J. P. M. Silva, K. A. Sakallah // The Best of ICCAD. — Springer, 2003. — С. 73—89.

99. An incremental approach to model checking progress properties [Текст] / A. R. Bradley [и др.] // Formal Methods in Computer-Aided Design (FMCAD),

2011. — IEEE. 2011. —С. 144—153.

100. Hassan, Z. Incremental, inductive CTL model checking [Текст] / Z. Hassan, A. R. Bradley, F. Somenzi // International Conference on Computer Aided Verification. — Springer. 2012. — С. 532—547.

101. Bradley, A. R. Understanding ic3 [Текст] / A. R. Bradley // International Conference on Theory and Applications of Satisfiability Testing. — Springer.

2012. — С. 1—14.

102. Cimatti, A. A lazy approach to temporal epistemic logic model checking [Текст] / A. Cimatti, M. Gario, S. Tonetta // Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems. — International Foundation for Autonomous Agents, Multiagent Systems. 2016. — С. 1218—1226.

103. Rescher, N.Epistemic logic: a survey of the logic of knowledge [Текст] / N. Rescher. — University of Pittsburgh Pre, 2005.

104. Balliu, M. Epistemic temporal logic for information flow security [Текст] / M. Balliu, M. Dam, G. Le Guernic // Proceedings of the ACM SIGPLAN 6th Workshop on Programming Languages and Analysis for Security. — ACM. 2011. —С. 6.

105. The nuXmv symbolic model checker [Текст] / R. Cavada [и др.] // International Conference on Computer Aided Verification. — Springer. 2014. — С. 334—342.

106. Vizel, Y. Lazy abstraction and SAT-based reachability in hardware model checking [Текст] / Y. Vizel, O. Grumberg, S. Shoham // Formal Methods in Computer-Aided Design (FMCAD), 2012. — IEEE. 2012. — С. 173—181.

107. Hassan, Z. Better generalization in IC3 [Текст] / Z. Hassan, A. R. Bradley, F. Somenzi // Formal Methods in Computer-Aided Design (FMCAD), 2013. — IEEE. 2013. —С. 157-164.

108. Welp, T. QF BV model checking with property directed reachability [Текст] / T. Welp, A. Kuehlmann // Proceedings of the Conference on Design, Automation and Test in Europe. — EDA Consortium. 2013. — С. 791—796.

109. IC3 modulo theories via implicit predicate abstraction [Текст] / A. Cimatti [и др.] // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2014. — С. 46—61.

110. Infinite-state invariant checking with IC3 and predicate abstraction [Текст] / A. Cimatti [и др.] // Formal Methods in System Design. — 2016. — Т. 49, № 3. — С. 190-218.

111. Ufo: A framework for abstraction-and interpolation-based software verification [Текст] / A. Albarghouthi [и др.] // International Conference on Computer Aided Verification. — Springer. 2012. — С. 672—678.

112. McMillan, K. L. Lazy annotation revisited [Текст] / K. L. McMillan // International Conference on Computer Aided Verification. — Springer. 2014. — С. 243-259.

113. Suda, M. Triggered clause pushing for IC3 [Текст] / M. Suda // arXiv preprint arXiv:1307.4966.-2013.

114. Cimatti, A. Software model checking via IC3 [Текст] / A. Cimatti, A. Griggio // International Conference on Computer Aided Verification. — Springer. 2012. — С. 277-293.

115. Lange, T. IC3 software model checking on control flow automata [Текст] / T. Lange, M. R. Neuhäußer, T. Noll // Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design. — FMCAD Inc. 2015. — С. 97-104.

116. Software model checking via large-block encoding [Текст] / D. Beyer [и др.] // 2009 Formal Methods in Computer-Aided Design. — IEEE. 2009. — С. 25—32.

117. Günther, H. Vienna verification tool: IC3 for parallel software [Текст] / H. Günther, A. Laarman, G. Weissenbacher // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2016. —С. 954-957.

118. Lazy sequentialization for the safety verification of unbounded concurrent programs [Текст] / T. L. Nguyen [и др.] // International Symposium on Automated Technology for Verification and Analysis. — Springer. 2016. — С. 174-191.

119. Бирюков, С. Анализ стратегий тестирования программного обеспечения [Текст] / С. Бирюков // Известия Южного федерального университета. Технические науки. — 2008. — Т. 78, № 1.

120. Godefroid, P. DART: directed automated random testing [Текст] / P. Godefroid, N. Klarlund, K. Sen // ACM Sigplan Notices. Т. 40. - ACM. 2005. -С. 213-223.

121. Липаев, В. Программная инженерия сложных заказных программных продуктов [Текст] / В. Липаев. — Directmedia, 2015.

122. Чепцов, М. Модель среды тестирования программного обеспечения при доказательстве функциональной безопасности систем управления движением поездов [Текст] / М. Чепцов // Сборник научных трудов Донецкого института железнодорожного транспорта. — 2006. — № 7.

123. An efficient 2-phase strategy to achieve high branch coverage [Текст] / S. Prabhu [и др.] // 2011 Asian Test Symposium. — IEEE. 2011. — С. 167—174.

124. Ломакина, Л. Модели и методы тестирования программного обеспечения на основе алгебраического подхода [Текст] / Л. Ломакина, А. Вигура // Системы управления и информационные технологии. — 2013. — Т. 52, №2—1. -С. 157-161.

125. Зыков, А. Применение системы klee для автоматизации тестирования программ на язык ах C/C++ [Текст] / А. Зыков, И. Кочетков, В. Поляков // Программные продукты и системы. — 2016. — 4 (116).

126. Басок, Б. М. Использование вероятностной модели вычислений для тестирования одного класса готовых к использованию программных компонентов локальных и сетевых систем [Текст] / Б. М. Басок, В. Н. Захаров, С. Л. Френкель // Информатика и её применения. — 2018. — Т. 12, № 4. —

C. 44-51.

127. Арутюнян, А. Сравнение эффективности обходчиков UniTESK [Текст] / А. Арутюнян // Труды института системного программирования РАН. — 2006.-Т. 10.

128. Кичигин, Д. Об одном методе сокращения набора тестов [Текст] / Д. Ки-чигин // Труды Института системного программирования РАН. — 2007. — Т. 13, № 1.

129. Демаков, А. Генерация тестовых данных сложной структуры с учетом контекстных ограничений [Текст] / А. Демаков, С. Зеленов, С. Зеленова // Труды Института системного программирования РАН. — 2006. — Т. 9.

130. Куцевол, В. Методология верификации протокола когерентности микропроцессора «Эльбрус^» [Текст] / В. Куцевол, А. Мешков, М. Петроченков // Вопросы радиоэлектроники», сер. ЭВТ. — 2013. — № 3. — С. 107—117.

131. Камкин, А. Тестирование в условиях неполной информации. Подход к разработке спецификаций и генерации тестов [Текст] / А. Камкин // Труды Института системного программирования РАН. — 2006. — Т. 10.

132. Godefroid, P. Compositional dynamic test generation [Текст] / P. Godefroid // ACM Sigplan Notices. Т. 42. — ACM. 2007. — С. 47—54.

133. Automated Whitebox Fuzz Testing. [Текст] / P. Godefroid, M. Y. Levin,

D. A. Molnar [и др.] // NDSS. Т. 8. — 2008. — С. 151—166.

134. Christakis, M. IC-Cut: A compositional search strategy for dynamic test generation [Текст] / M. Christakis, P. Godefroid // International SPIN Workshop on Model Checking of Software. — Springer. 2015. — С. 300—318.

135. Kroening, D. Formal verification of SystemC by automatic hardware/software partitioning [Текст] / D. Kroening, N. Sharygina // Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design. — IEEE Computer Society. 2005. — С. 101—110.

136. Курейчик, В. Генетические алгоритмы [Текст] / В. Курейчик // Известия Южного федерального университета. Технические науки. — 1998. — Т. 8, № 2.

137. Курейчик, В. В. Биоиспирированный поиск при проектировании и управлении [Текст] / В. В. Курейчик, В. В. Курейчик // Известия Южного федерального университета. Технические науки. — 2012. — Т. 136, 11 (136).

138. Тестирование программ с использованием генетических алгоритмов [Текст] / Б. Палюх [и др.] // Программные продукты и системы. — 2011. — № 4.

139. Литвиненко, А. Генерация данных для тестирования программ с использованием эволюционных алгоритмов [Текст] / А. Литвиненко, К. Сметанин // Modern science: Theoretical and practical look. — 2018. — С. 86—88.

140. Курейчик, В. Модифицированные генетические операторы [Текст] / В. Курейчик // Известия Южного федерального университета. Технические науки. — 2009. — Т. 101, № 12.

141. Шкамардин, И. Генетические алгоритмы с представлением переменной длины [Текст] / И. Шкамардин // Известия Южного федерального университета. Технические науки. — 2007. — Т. 73, № 1.

142. Карпушинский, А. М. Применение генетических алгоритмов при генерации тестов для программ, содержащих обработку исключений [Текст] / А. М. Карпушинский, Т. А. Павловская // Научно-технический вестник информационных технологий, механики и оптики. — 2011. — 4 (74).

143. Владимиров, М. Критерии полноты тестового покрытия в генетических алгоритмах генерации тестов [Текст] / М. Владимиров // Труды Института системного программирования РАН. — 2006. — Т. 9.

144. Пантелеев, А. В. Применение генетических алгоритмов с бинарным и вещественным кодированием для приближенного синтеза субоптимального управления детерминированными системами [Текст] / А. В. Пантелеев,

Д. В. Метлицкая // Автоматика и телемеханика. — 2011. — № 11. — С. 117-129.

145. Говорущенко, Т. О. Процесс повторного тестирования в процессе экспертизы программного обеспечения [Текст] / Т. О. Говорущенко // Системы дослщження та шформацшш технологи. — 2011. — № 1. — С. 71—86.

146. Кулямин, В. Организация сложных тестовых наборов [Текст] / В. Кулямин // Труды Института системного программирования РАН. — 2009. — Т. 17.

147. Верификация в исследовательских, учебных и промышленных системах [Текст] / О. Немолочнов [и др.] // Научно-технический вестник информационных технологий, механики и оптики. — 2003. — № 11.

148. Подход UniTesK к разработке тестов: достижения и перспективы [Текст] / И. Бурдонов [и др.] // Труды Института системного программирования РАН. — 2004. — Т. 5.

149. Автоматическая генерация тестов для графического пользовательского интерфейса по ЦМЬ диаграммам действий [Текст] / А. Калинов [и др.] // Труды Института системного программирования РАН. — 2004. — Т. 8, № 1.

150. Немолочнов, О. Кубические покрытия логических условий вычислительных процессов и программ [Текст] / О. Немолочнов, А. Зыков, В. Поляков // Научно-технический вестник информационных технологий, механики и оптики. — 2004. — № 14.

151. Графо-аналитические модели вычислительных процессов в САПР [Текст] / А. Г. Зыков [и др.] // Научно-технический вестник информационных технологий, механики и оптики. — 2011. — 4 (74).

152. Параллельные структуры управления вычислительными процессами в САПР [Текст] / О. Немолочнов [и др.] // Научно-технический вестник информационных технологий, механики и оптики. — 2011. — 4 (74).

153. Оценка сложности графа функциональной программы [Текст] / А. В. Лаз-дин, О. Немолочнов [и др.] // Научно-технический вестник информационных технологий, механики и оптики. — 2002. — № 6.

154. Методы тестирования вычислительных процессов [Текст] / О. Немолочнов [и др.] // Научно-технический вестник информационных технологий, механики и оптики. — 2007. — № 45.

155. Иванов, В. Разработка среды дореализационного моделирования и тестирования программного обеспечения [Текст] / В. Иванов, А. Ныцик // Системи обробки шформацн. — 2010. — № 9. — С. 40—43.

156. Зайцев, Д. универсальная сеть Петри [Текст] / Д. Зайцев // Кибернетика и системный анализ. — 2012.

157. Применение технологии UniTesK для функционального тестирования моделей аппаратного обеспечения [Текст] / В. Иванников [и др.] // Москва. — 2005.— Т. 19.

158. Использование формальных методов для обеспечения соблюдения программных стандартов [Текст] / А. Гриневич [и др.] // Труды Института системного программирования РАН. — 2006. — Т. 10.

159. Силаков, Д. Автоматизация тестирования web-приложений, основанных на скриптовых языках [Текст] / Д. Силаков // Труды Института системного программирования РАН. — 2008. — Т. 14, № 2.

160. Баранцев, А. Генерация оптимизированных для ручного выполнения сценариев тестирования приложений с графическим интерфейсом пользователя [Текст] / А. Баранцев, С. Грошев, В. Омельченко // Труды Института системного программирования РАН. — 2009. — Т. 17.

161. Зеленов, С. Автоматическая генерация тестовых данных для оптимизаторов графических моделей [Текст] / С. Зеленов, Д. Силаков // Труды Института системного программирования РАН. — 2006. — Т. 9.

162. Хорошилов, А. Спецификация и тестирование систем с асинхронным интерфейсом [Текст] / А. Хорошилов // Москва. — 2006. — Т. 17.

163. Метод обнаружения недекларированных возможностей и значений don't care вычислительного процесса [Текст] / О. Немолочнов [и др.] // Известия высших учебных заведений. Приборостроение. — 2009. — Т. 52, № 12.

164. Кризис промышленной технологии программирования, недекларирован-ные возможности и don't care [Текст] / О. Немолочнов, Л. Г. Осовец-кий [и др.] // Известия высших учебных заведений. Приборостроение. — 2014.— Т. 57, № 1.

165. Поиск процедур по графу переходов функциональной программы при верификации вычислительных процессов [Текст] / А. А. Гедич [и др.] //Известия высших учебных заведений. Приборостроение. — 2014. — Т. 57, № 4.

166. Петров, К. Моделирование логических неисправностей в циклах вычислительных процессов программ [Текст] / К. Петров // Научно-технический вестник информационных технологий, механики и оптики. — 2006. — № 25.

167. Верещагин, Н. Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции. [Текст] / Н. Верещагин, А. Шень. — MCCME Publishers, Moscow, 2017.

168. Turing, A. M. On computable numbers, with an application to the Entscheidungsproblem [Текст] / A. M. Turing // Proceedings of the London mathematical society. — 1937. — Т. 2, № 1. — С. 230—265.

169. Коварцев, А. Тестирование математических моделей вычислительных алгоритмов на основе метода глобальной оптимизации [Текст] / А. Коварцев, Д. Попова-Коварцева, Е. Серповская // Информационные технологии и на-нотехнологии. — 2015. — С. 191—196.

170. Камкин, А. Метод построения тестового оракула для подсистемы памяти микропроцессора на основе недетерминированной функциональной модели [Текст] / А. Камкин, М. Петроченков // Вопросы радиоэлектроники. — 2015.—№3. —С. 84.

171. Иванников, В. П. Проверка корректности поведения HDL-моделей цифровой аппаратуры на основе динамического сопоставления трасс [Текст] / В. П. Иванников, А. С. Камкин, М. М. Чупилко // Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Информатика. Телекоммуникации. Управление. — 2014. — 2 (193).

172. Testing systems specified as partial order input/output automata [Текст] / G. v. Bochmann [и др.] // Testing of software and communicating systems. — Springer, 2008. - С. 169-183.

173. Казьмина, С. К. Компактное тестирование [Текст] / С. К. Казьмина// Автоматика и телемеханика. — 1982. — № 3. — С. 173—189.

174. Поляков, Г. Методика комплексной семантико-числовой верификации си программ и их временных параллельных моделей [Текст] / Г. Поляков, Д. Толстолужский // Радюелектронш i комп'ютерш системи. — 2009. — № 7. - С. 240-244.

175. Majumdar, R. Reducing test inputs using information partitions [Текст] / R. Majumdar, R.-G. Xu // International Conference on Computer Aided Verification. — Springer. 2009. — С. 555—569.

176. Blasum, H. Gcov on an embedded system [Текст] / H. Blasum, F. Gorgen, J. Urban // GCC for Research in Embedded and Parallel Systems. — 2007.

177. Блау, С. А. Эффективность тестирования структуры программных модулей [Текст] / С. А. Блау, В. В. Липаев, Б. А. Позин // Автоматика и телемеханика. - 1984. - № 4. - С. 139-148.

178. Carter, J. L. Universal classes of hash functions [Текст] / J. L. Carter, M. N. Wegman // Journal of computer and system sciences. — 1979. — Т. 18, № 2. — С. 143-154.

179. Асанов, М. Дискретная математика: графы, матроиды, алгоритмы [Текст] / М. Асанов, В. Баранский, В. Расин // Ижевск: НИЦ «Регулярная и хаотическая динамика. — 2001. — Т. 288.

180. Sanyal, A. Data flow analysis: theory and practice [Текст] / A. Sanyal, B. Sathe, U. Khedker. - CRC Press, 2009.

181. Allen, F. E. A program data flow analysis procedure [Текст] / F. E. Allen, J. Cocke // Communications of the ACM. — 1976. — Т. 19, № 3. — С. 137.

182. Damaggio, E. Artifact systems with data dependencies and arithmetic [Текст] / E. Damaggio, A. Deutsch, V. Vianu // ACM Transactions on Database Systems (TODS). - 2012. - Т. 37, № 3. - С. 22.

183. Chakrabarti, A. Software partitioning for effective automated unit testing [Текст] / A. Chakrabarti, P. Godefroid // Proceedings of the 6th ACM & IEEE International conference on Embedded software. —ACM. 2006. — С. 262—271.

184. Parnas, D. L. Really rethinking'formal methods' [Текст] / D. L. Parnas // Computer. — 2010. — Т. 43, № 1. — С. 28—34.

185. Гедич, А. А. Автоматический поиск локальных переменных и аргументов процедуры в исполняемом коде программы при верификации вычислительных процессов [Текст] / А. А. Гедич, А. Г. Зыков, А. В. Лаздин // Научно-технический вестник информационных технологий, механики и оптики. — 2013.-5 (87).

186. Камкин, А. Система поддержки верификации реализаций протоколов когерентности с использованием формальных методов. [Текст] / А. Камкин, М. Петроченков // Вопросы радиоэлектроники. — 2014. — Т. 4, № 3. —

C. 27—38.

187. Попова, Ю. Тестирование и отладка программного обеспечения [Текст] / Ю. Попова. — 2010.

188. Гусеница, Я. Алгоритм поиска зон в управляющих графах [Текст] / Я. Гусеница // Информатика и системы управления. — 2017. — № 3. — С. 119—124.

189. Ложкин, С. А. Лекции по основам кибернетики [Текст] / С. А. Ложкин. — Издат. отд. Фак. ВМиК МГУ им. МВ Ломоносова М., 2004.

190. Структурирование программ и вычислительных процессов на множество линейных и условных вершин [Текст] / О. Немолочнов [и др.] // Научно-технический вестник информационных технологий, механики и оптики. —— 2005. — № 19.

191. Staples, /.Computation on graph-like expressions [Текст] / J. Staples // Theoretical Computer Science. — 1980. — Т. 10, № 2. — С. 171—185.

192. Call graph construction in object-oriented languages [Текст] / D. Grove [и др.] // ACM SIGPLAN Notices. — 1997. — Т. 32, № 10. — С. 108—124.

193. Constructing the procedure call multigraph [Текст] / D. Callahan [и др.] // IEEE Transactions on Software Engineering. — 1990. — Т. 16, № 4. — С. 483—487.

194. Агрессивная инлайн-подстановка функций для VLIW-архитектур [Текст] / А. Ермолицкий [и др.] // Труды Института системного программирования РАН. — 2015. — Т. 27, №6.

195. Bacon, D. F. Fast static analysis of C++ virtual function calls [Текст] /

D. F. Bacon, P. F. Sweeney //ACM SigplanNotices. — 1996. — Т. 31, № 10. — С. 324—341.

196. Русяев, Р. Особенности реализации механизма обработки исключений C++ для платформы «Эльбрус» [Текст] / Р. Русяев, С. Баранников, М. Нейман-заде // Вопросы радиоэлектроники. — 2018. — № 2. — С. 45—50.

197. Павловская, Т. Построение управляющего графа программы, содержащей неявный поток управления [Текст] / Т. Павловская, А. Карпушинский // Научно-технический вестник информационных технологий, механики и опти ки. — 2008. — № 48.

198. Richardson, L. RESTful web services [Текст] / L. Richardson, S. Ruby. — "O'Reilly Media, Inc.", 2008.

199. Lattner, C. LLVM and Clang: Next generation compiler technology [Текст] / C. Lattner // The BSD conference. — 2008. — С. 1—2.

200. Волконский, В. Оптимизирующие компиляторы для архитектуры с явным параллелизмом команд и аппаратной поддержкой двоичной совместимости [Текст] / В. Волконский // Информационные технологии и вычислительные системы. — 2004. — Т. 3.

201. Sleator, D. D. Self-adjusting heaps [Текст] / D. D. Sleator, R. E. Tarjan // SIAM Journal on Computing. — 1986. — Т. 15, № 1. — С. 52—69.

202. Carlsson, S. An implicit binomial queue with constant insertion time [Текст] / S. Carlsson, J. I. Munro, P. V. Poblete // Scandinavian Workshop on Algorithm Theory. — Springer. 1988. — С. 1—13.

203. Wagner, R. A. The string-to-string correction problem [Текст] / R. A. Wagner, M. J. Fischer // Journal of the ACM (JACM). — 1974. — Т. 21, № 1. — С. 168-173.

204. Ukkonen, E. Finding approximate patterns in strings [Текст] / E. Ukkonen // Journal of algorithms. — 1985. — Т. 6, № 1. — С. 132—137.

205. Perplexity—a measure of the difficulty of speech recognition tasks [Текст] / F. Jelinek [и др.] // The Journal of the Acoustical Society of America. — 1977. — Т. 62, № 1.-С. 63-63.

206. Колмогоров, А. Н. Три подхода к определению понятия "количество информации" [Текст] / А. Н. Колмогоров // Проблемы передачи информации. — 1965.-Т. 1, № 1.-С. 3-11.

207. Cognitive and sub-regular complexity [Текст] / J. Rogers [и др.] // Formal grammar. — Springer. 2013. — С. 90—108.

208. Kondrak, G. N-gram similarity and distance [Текст] / G. Kondrak // International symposium on string processing and information retrieval. — Springer. 2005. — С. 115—126.

209. Levenshtein, V. I. Binary codes capable of correcting deletions, insertions, and reversals [Текст] / V. I. Levenshtein // Soviet physics doklady. Т. 10. — 1966. — С. 707—710.

210. Needleman, S. B. A general method applicable to the search for similarities in the amino acid sequence of two proteins [Текст] / S. B. Needleman, C. D. Wunsch// Journal of molecular biology. — 1970. — Т. 48, № 3. — С. 443—453.

211. Поляков, В. И. Преобразование моделей алгоритмов [Текст] / В. И. Поляков, В. И. Скорубский // Известия высших учебных заведений. Приборостроение. — 2012. — Т. 55, № 10.

212. Zhang, F. Using hammock graphs to structure programs [Текст] / F. Zhang, E. H. D'Hollander // IEEE Transactions on Software Engineering. — 2004. — Т. 30, № 4. — С. 231—245.

213. A survey of graph edit distance [Текст] / X. Gao [и др.] // Pattern Analysis and applications. — 2010. — Т. 13, № 1. — С. 113—129.

214. Gotoh, O. An improved algorithm for matching biological sequences [Текст] / O. Gotoh// Journal of molecular biology. — 1982. — Т. 162, № 3. — С. 705—708.

Список рисунков

1.1 Пример замены выражения на булеву переменную............ 17

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

1.3 Общий вид цикла верификации программы, реализующего

парадигму CEGAR..............................25

1.4 Последовательные пути выполнения тестируемой программы в примере DART. Целенаправленно выбираемый префикс пути

отмечен пунктиром ............................. 57

1.5 Блок-схема программы к примеру партиционирования .........67

2.1 Пример программы, требующей перебора переходов .......... 82

2.2 Пример зависимости времени тестирования от полноты покрытия ветвлений в алгоритме без ограничения числа реальтернаций ...... 87

2.3 Примеры ускорения покрытия ветвей при ограничении реальтернаций 88

2.4 Примеры зависимости времени тестирования от полноты покрытия ветвлений при различных значениях разрешенного числа повторных обходов.................................... 89

2.5 Примеры зависимости числа тестов от лимита реальтернаций для примера программы ............................. 90

2.6 Пример программы с циклом, в которой ошибка гарантированно обнаруживается даже при ограничении реальтернаций ......... 92

2.7 Пример программы с циклом, в которой ошибка может остаться необнаруженной при ограничении реальтернаций ............ 93

2.8 Иллюстрация выделения эффективного контекста для условного перехода ................................... 94

2.9 Пример многониточной организации тестов ............... 101

2.10 Иллюстрация распространения символических значений

в релевантном условию y = 3 подграфе графа зависимостей по

итогам запусков тестов для примера программы.............102

3.1 Пример принятия решений о необходимости (а) и необязательности

(б) альтернации ...............................108

3.2 Пример репрезентативной структуры...................112

3.3 Пример блочной структуры программы..................115

3.4 Пример аннотирования графа управления. Сплошные стрелки соответствуют рёбрам, входящим в остовное дерево; пунктирные -прочим рёбрам................................118

3.5 Пример построения (несбалансированного) остовного дерева

в случае, когда граф управления представляет собой цепочку гамаков . 120

3.6 Пример построения бинарного дерева для остовного дерева графа управления (соответствует примеру, показанному на рис. 3.5) .....121

3.7 Пример представления двух куч и их объединения с использованием общего графа выражений .......................... 124

3.8 Примерная схема интеграции фильтра на основе функции £ в цикл направленного тестирования ........................ 129

3.9 Схема обработки прерываний в стандартном программном интерфейсе Itanium ABI на входе преобразователя интерфейса (a)

и после статических подстановок, выполненных преобразователем (б) 132

3.10 Алгоритм поиска множества вершин D(V +,V-).............135

3.11 Пример поиска в графе с построенным остовным деревом

и запрещёнными вершинами и соответствующая ему образная аналогия включения интервалов ...................... 137

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

3.13 Соотношение потока интервалов на входе и выходе очереди......141

3.14 Количество вовлечённых в поиск функций................141

4.1 Пример единичного шага выравнивания автомата и строки.......150

4.2 Пример трансдьюсера и соответствующей электронной схемы, реализующей распределение токов, аналогичное распределению

потока подкрепления в фазе 2 алгоритма ................. 155

4.3 Пример различия эффективного и структурного графа управления . . . 156

4.4 Пример кода и восстановленного для него графа управления......157

4.5 Пример кода с множественными вызовами функции и построенной

для него аппроксимации графа управления................159

4.6 Отличие реального графа управления для примера программы (а)

и его приближения, удовлетворяющего регулярному выражению (б) . .161

4.7 Пример графа регулярного выражения ..................163

4.8 Пример редактирования графа регулярного выражения: добавление строки "гх12е"к выражению /ах(Ье|с^/ ..................168

4.9 Алгоритм построения графа регулярного выражения..........169

4.10 Процедура добавления ветви в граф регулярного выражения......170

4.11 Процедура рекурсивного поиска повторяющихся фрагментов......172

Список таблиц

1 Список темпоральных операторов..................... 15

2 Конкретные алгоритмы как примеры общего подхода

к инкрементальной индуктивной верификации (согласно [101]) .... 48

3 Среднее число итераций поиска и сложность перебора интервалов для различных используемых деревьев и критериев приоритета

очереди интервалов ............................. 140

4 Сравнение (в средних числах операций на вершину) эффективности реализации хранения множеств £ в зависимости от типа контейнера . . 143

5 Операции редактирования ......................... 165