2.tex

\chapter{Подготовка верификационных задач}

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

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

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

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

Программным интерфейсом модуля будем называть следующие глобальные переменные, функции, типы и макросы:
\begin{itemize}
    \item Функции относятся к программному интерфейсу, если они не определены в исходном коде модуля, но вызываются в нем. Определенные в исходном коде модуля функции, которые вызываются в окружении, будем называть \textit{точками входа}.
    Точки входа тоже являются частью программного интерфейса модуля.
    \item Аналогично макросы относятся к программному интерфейсу, если соответствующие макроподстановки используются и в окружении, и в исходном коде модуля.
    \item Параметры макрофункций и функций программного интерфейса тоже являются частью программного интерфейса модуля.
    \item Тип относится к программному интерфейсу, если он используется и в исходном коде модуля, и в окружении.
    Стандартные типы языка Си не относятся к программному интерфейсу модуля.
    \item К программному интерфейсу модуля относятся глобальные переменные, доступ к которым осуществляется и в исходном коде модуля, и в окружении.
\end{itemize}

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

Рассмотрим пример модуля программы и его программный интерфейс:
\begin{lstlisting}[language=C,basicstyle=\small]
extern int b;
extern int f4(int a, int b);
int f1(int a, int b);
int f2(int a, int b);
static int f3(int a, int b)

int f1(int a) {
    return f3;
}

int f2(int a) {
    int c;
    
    c = nondet_int();
    return f4(a, c);
}

static int f3(int a) {
    if (a < b)
        return a - b;
    else
        return b - a;
}
\end{lstlisting}

Функции \textit{f1}, \textit{f2}, \textit{f4}, \textit{nondet\_int}, параметры функций и переменная \textit{b} определяют программный интерфейс данного модуля. 
Функции \textit{f1} и \textit{f2} являются точками входа, так как могут быть вызваны в окружении.
Функция \textit{f4} определена и переменная \textit{b} инициализирована в окружении, так как определение \textit{f4} и инициализация \textit{b} отсутствуют в примере.

Назовем \textit{событиями взаимодействия} модуля и окружения следующие операции на языке программирования Си:
\begin{itemize}
    \item Вызовы функций и макрофункций программного интерфейса модуля.
    \item Обращения на чтение или запись к глобальным переменным программного интерфейса модуля и к областям памяти в куче или на стеке, с указателями на которые выполняются операции и в исходном коде модуля, и в окружении.
\end{itemize}

\textit{Сценариями взаимодействия} модуля и окружения называются последовательности событий взаимодействия модуля и окружения, которые могут происходить при реальном выполнении программы, содержащей рассматриваемый модуль.
Сценарии взаимодействия, как правило, допускают разные пути выполнения программы с различными последовательностями событий взаимодействия в каждом из них.
К последовательностям событий в рамках сценария взаимодействия можно сформулировать следующие виды требований:
\begin{itemize}
    \item Ограничения на порядок следования событий взаимодействия, которые определяются:
        \begin{itemize}
            \item Отношениями до или после. Например, вызов одной функции происходит строго после другой. 
            \item Отношениями по возможности параллельного выполнения событий взаимодействия. Например, некоторые события выполняются параллельно или строго в одном и том же потоке или процессе программы.
            \item Отношениями зависимости событий, то есть события могут возникать обязательно или взаимоисключающим образом относительно друг друга. Например, вызов некоторой точки входа модуля программы выполняется строго при условии захвата определенного мютекса или другого механизма синхронизации.
        \end{itemize}
    \item События взаимодействия зависят по данным:
        \begin{itemize}
            \item В качестве параметров функций должны передаваться одни и те же значения или указатели на одну и ту же память. При выполнении доступа на чтение или запись должны быть прочитаны или записаны определенные данные.
            \item Могут быть справедливы ограничения на значения параметров функций и содержание определенных областей памяти. 
            Примером такого ограничения является требование, что некоторая точка входа модуля программы может быть вызвана с произвольным целым неотрицательным параметром.
        \end{itemize}
\end{itemize}

\textit{Моделью окружения} называется вспомогательный исходный код на языке программирования Си, который реализует сценарии взаимодействия модуля и окружения.
Такой код может состоять из отдельного файла, набора файлов или может быть представлен в виде отдельных фрагментов кода, предназначенных для вставки в исходный код модуля программы при помощи инструментации.
Любое описание модели окружения или ее модулей на каком-либо языке предметной области будем называть спецификацией модели окружения.

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

Для преобразующих программ, у которых точкой входа является main, моделирование окружения сводится к разработке моделей функций, которые вызываются в исходном коде модуля и определены окружением.
Модель окружения для модулей библиотек и событийно-ориентированных программ имеет, как правило, более сложное устройство.
Для иллюстрации процесса моделирования окружения таких модулей рассмотрим следующий пример:
\begin{lstlisting}[language=C,basicstyle=\small]
/* drivers/tty/tty_io.c */
LIST_HEAD(tty_drivers);
struct tty_driver *tty_alloc_driver(...) {
	struct tty_driver *driver = kzalloc(...);
	if (!driver)
		return ERR_PTR(-ENOMEM);
	return driver;
}
void tty_set_operations(struct tty_driver *driver, 
                        struct tty_operations *op) {
	driver->ops = op;
};
void put_tty_driver(struct tty_driver *d) {
	kfree(d);
}
int tty_register_driver(struct tty_driver *driver) {
	list_add(&driver->tty_drivers, &tty_drivers);
	return 0;
}
int tty_unregister_driver(struct tty_driver *driver) {
	list_del(&driver->tty_drivers);
	return 0;
}
int __init tty_init(void) {
	...
	return 0;
}
\end{lstlisting}

Данный пример построен на основе файла \textit{drivers/tty/tty\_io.c} подсистемы TTY ядра ОС Linux версии 3.14.79.
Будем называть его модулем подсистемы.
Точками входа модуля подсистемы являются функции \textit{tty\_alloc\_driver}, \textit{tty\_set\_operations}, \textit{tty\_register\_driver}, \textit{tty\_unregister\_driver}, \textit{put\_tty\_driver}, используемые драйверами, и функция \textit{tty\_init}, которую вызывает ядро ОС на этапе загрузки.
Каждый вызов точки входа подсистемы является событием сценария взаимодействия модуля подсистемы и окружения, который назовем сценарием вызова библиотечных функций.
Сценарий, состоящий из одного события вызова функции инициализации подсистемы, назовем сценарием инициализации подсистемы.
Таким образом, модель окружения должна содержать модели двух сценариев, реализующих последовательности вызова точек входа.
Рассмотрим пример последовательности событий взаимодействия сценария вызова библиотечных функций, в которой функции подсистемы вызываются в следующем порядке для одного и того же указателя \textit{driver}:
\begin{enumerate}
    \item В начале вызывается функция выделения памяти \textit{tty\_alloc\_driver}, возвращающая указатель \textit{driver}.
    \item Затем выполняется сохранение указателя на структуру с обработчиками драйвера в структуре, на которую указывает указатель \textit{driver}, при помощи вызова \textit{tty\_set\_operations}.
    \item Затем следует регистрация обработчиков, выполняемая при помощи вызова функции \textit{tty\_register\_driver}, после которой ядро операционной системы может вызывать зарегистрированные обработчики.
    \item Дерегистрация обработчиков выполняется при помощи \textit{tty\_unregister\_driver}.
    \item В конце выполняется освобождение памяти при помощи вызова функции \textit{put\_tty\_driver}.
\end{enumerate}

Простейшая модель окружения для данного примера будет иметь вид:
\begin{lstlisting}[language=C,basicstyle=\small]
int main(void) {
    int ret;
    struct tty_driver *driver;
    struct tty_operations *ops;
    ret = tty_init();
    if (ret)
        goto exit;
    ops = __VERIFIER_nondet_pointer();
    driver = tty_alloc_driver(...);
    if (driver == 0)
        goto exit;
    tty_set_operations(driver, ops);
    if (tty_register_driver(driver))
        goto clean;
    tty_unregister_driver(driver);
clean:
    put_tty_driver(driver);
exit:
    return 0;
}
\end{lstlisting}

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

Теперь рассмотрим модуль драйвера, вызывающего точки входа рассматриваемого модуля подсистемы:
\begin{lstlisting}[language=C,basicstyle=\small]
/* drivers/tty/moxa.c */
static const struct tty_operations moxa_ops = {
	.open = moxa_open,
	.close = moxa_close,
	.write = moxa_write
};
static struct tty_driver *moxaDriver;
static int __init moxa_init(void) {
	int retval = 0;
	moxaDriver = tty_alloc_driver(...);
	if (IS_ERR(moxaDriver))
		return PTR_ERR(moxaDriver);
    tty_set_operations(moxaDriver, &moxa_ops);
    if (tty_register_driver(moxaDriver)) {
		put_tty_driver(moxaDriver);
		return -1;
	}
	return 0;
}
static void __exit moxa_exit(void) {
    tty_unregister_driver(moxaDriver);
	put_tty_driver(moxaDriver);
}
module_init(moxa_init);
module_exit(moxa_exit);
\end{lstlisting}

Модуль основан на исходном коде файла драйвера \textit{drivers/tty/moxa.c} ядра ОС Linux версии 3.14.79.
В данном модуле точками входа являются обработчики \textit{moxa\_open}, \textit{moxa\_close}, \textit{moxa\_write} и функции инициализации и выхода драйвера \textit{moxa\_init} и \textit{moxa\_exit}.
Для данного модуля можно определить два сценария взаимодействия модуля и окружения: сценарий вызова обработчиков и сценарий инициализации и выхода драйвера.
Сценарий инициализации и выхода драйвера состоит из двух событий взаимодействия: вызова функции инициализации драйвера при загрузке драйвера в память и события вызова функции выхода при выгрузке драйвера из памяти.
Сценарий вызова обработчиков может быть выполнен окружением строго после успешного вызова функции \textit{tty\_register\_driver} и до вызова функции \textit{tty\_unregister\_driver}.
Рассматриваемый модуль драйвера реализует последовательность вызова библиотечных функций из соответствующего сценария взаимодействия модуля подсистемы.
 
Если требуется верифицировать два модуля вместе, то необходимо моделировать меньше сценариев взаимодействия, так как события сценария вызова библиотечных функций уже не выполняются окружением, а выполнены в исходном коде модуля драйвера.
В то же время возникают дополнительные требования к допустимым последовательностям событий из разных сценариев взаимодействия.
Например, сценарий инициализации подсистемы выполняется всегда строго до сценария инициализации и выхода драйвера. То есть точка входа модели окружения должна вызвать функцию инициализации драйвера \textit{moxa\_init} строго после завершения работы функции инициализации подсистемы \textit{tty\_init}.
Данные рассуждения являются упрощенными и неполными, например, не рассматриваются ограничения по данным и отношения возможности параллельного выполнения функций.

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

\section{Схема генерации верификационных задач}

В данном разделе рассматривается генерация верификационных задач, которая выполняется \textit{генератором верификационных задач}, схема работы которого представлена на рисунке~\ref{figure:vt_generator}.
Входными данными генератора являются:
\begin{itemize}
    \item База сборки программы, которая содержит структурированную информацию о процессе сборке верифицируемой программной системы на языке программирования Си и ее составе, включая сами файлы с исходным кодом.
    \item Конфигурационные параметры для адаптации процесса генерации верификационных задач в зависимости от проверяемых требований и программной системы.
    \item Спецификация декомпозиции, разработанная пользователем для уточнения состава модулей программной системы.
    \item Спецификации предположений об окружении, заданные на языке предметной области.
    \item Спецификации требований с формальным описанием каждого проверяемого требования.
\end{itemize}

\begin{figure}
\centering
\includegraphics[scale=1]{vt_generator}
\caption{Схема генератора верификационных задач.}
\label{figure:vt_generator}
\end{figure}

Программные системы на языке Си, как правило, распространяются в виде файлов с исходным кодом и скриптов для их компиляции и компоновки.
Для получения информации об устройстве такой системы выполняется контролируемая сборка, в ходе которой подготавливается \textit{база сборки}.
В рамках данного метода процесс сбора такой базы не рассматривается и предлагается использовать для этого доступные инструменты.
База сборки должна содержать следующие данные в своем составе:
\begin{itemize}
    \item файлы с исходным кодом программной системы на языке программирования Си;
    \item команды компиляции и компоновки в виде графа зависимостей между командами сборки;
    \item описание программного интерфейса файлов программной системы.
    \end{itemize}
    
В базе сборки сохраняются все файлы программной системы с расширением <<.c>> и заголовочные файлы зависимостей, необходимые для выполнения препроцессирования.

Пример фрагмента графа зависимостей между командами сборки изображен на рисунке \ref{figure:cbg}.
Граф является ориентированным и его вершинам соответствуют файлы, которые являются входными и выходными файлами команд сборки, а ребра графа соответствуют самим командам сборки.
Граф должен включать не только команды компиляции и компоновки, но и команды перемещения, удаления, переименования файлов и т.п.
Наличие ребра в графе между двумя вершинами означает, что некоторая команда сборки принимает на вход исходный файл и получает на выходе новый файл.
В составе графа хранится вспомогательная информация о командах сборки, например, опции команд, путь к директории выполнения, значения переменных окружения.
Если граф построен корректно, то в графе нет ребер направленных к вершинам, которые соответствуют файлам с исходным кодом, а вершины, соответствующие финальным исполняемым файлам программной системы, не содержат исходящих ребер.

\begin{figure}
\centering
\includegraphics[scale=2]{cbg}
\caption{Фрагмент графа зависимостей команд сборки апплетов проекта BusyBox.}
\label{figure:cbg}
\end{figure}

Описание программного интерфейса программной системы представляет собой структурированные данные о составе каждого файла с исходным кодом, которые содержат:
\begin{itemize}
    \item Список деклараций и определений функций вместе с их сигнатурами.
    \item Граф вызова функций. Для каждого вызова должна быть сохранена информация о вызываемой и вызывающей функциях.
    Параметры вызова сохраняются в том случае, если среди них есть указатели на глобальные переменные или функции.
    \item Список инициализируемых глобальных переменных и их декларации.
    \item Список макросов и макроподстановок сохраняется аналогично списку определений и деклараций функций.
    \item Список определений и области видимости типов, определенных в программной системе.
\end{itemize}

Результатом работы генератора верификационных задач является набор верификационных задач в формате сообщества SV"~COMP.
Процесс генерации верификационных задач состоит из 4 шагов:
\begin{enumerate}
    \item На первом шаге в процессе декомпозиции определяются модули программной системы. 
    \item Затем для каждого модуля выполняется подготовка модели окружения на языке программирования Си.
    \item После моделей окружения синтезируются модели требований на языке программирования Си.
    \item Заключительным шагом является компоновка полученных на предыдущих шагах данных для получения верификационных задач в заданном формате.
\end{enumerate}

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

\section{Метод декомпозиции Си-программ на модули}
В данном разделе представлен метод автоматизированной декомпозиции Си-программ на модули, нацеленный на решение следующих задач:
\begin{itemize}
    \item выделить часть исходного кода программной системы, которую требуется верифицировать;
    \item декомпозировать выделенную часть исходного кода программной системы на модули, которые инструменты верификации моделей программ способны проверить по отдельности в составе верификационных задач.
\end{itemize}

Результат декомпозиции программной системы характеризуется следующими показателями:
\begin{itemize}
    \item \textit{Число полученных модулей}. Чем модулей меньше, тем, как правило, меньше времени потребуется на верификацию и ниже трудозатраты на моделирование окружения.
    \item \textit{Трудозатраты на моделирование окружения}. Трудозатраты зависят от сложности программного интерфейса модулей. Чем больше число точек входа и неопределенных функций в каждом модуле, тем больше моделей сценариев взаимодействия и неопределенных функций требуется подготовить пользователю.
    \item \textit{Число таких модулей, верификационные задачи на основе которых могут быть решены инструментом верификации моделей программ}.
\end{itemize}

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

Для декомпозиции программной системы на языке Си предлагается выполнять следующие шаги:
\begin{enumerate}
    \item определить файлы и функции в составе программы;
    \item выделить модули;
    \item выбрать целевые модули;
    \item скорректировать состав модулей согласно спецификации декомпозиции;
    \item агрегировать модули.
\end{enumerate}

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

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

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

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

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

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

Затем выполняется шаг коррекции состава модулей, который является необязательным и выполняется в том случае, если пользователь подготовил спецификацию декомпозиции.
Спецификация декомпозиции может содержать следующие команды:
\begin{itemize}
    \item Добавить или заменить состав файлов модуля с определенным именем.
    \item Добавить или удалить определенные файлы из модуля с некоторым именем.
    \item Удалить определенные файлы из всех модулей.
    \item Добавить определенные файлы ко всем модулям.
\end{itemize}

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

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

Последним шагом является агрегация модулей.
На данном шаге выполняется для каждого целевого модуля поиск наборов модулей, которые могут включать и нецелевые модули, согласно некоторой \textit{стратегии агрегации}.
Стратегия реализует алгоритм для выбора модулей, чтобы либо снизить число точек входа целевого модуля, либо снизить число неопределенных функций при объединении модулей из набора в новый модуль.
Агрегация нацелена на сокращение трудоемкости моделирования окружения при помощи верификации модулей вместе.
При разработке стратегии стоит учесть, что увеличение числа наборов объединенных модулей приводит к увеличению времени верификации, а увеличение размера наборов повышает риск возникновения взрыва числа состояний в модели, построенной инструментом верификации на основе исходного кода объединенных модулей.

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

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

\begin{figure}
\centering
\includegraphics[scale=1.2]{decomposition_example}
\caption{Пример декомпозиции фрагмента проекта BusyBox на модули.}
\label{figure:decomposition_example}
\end{figure}

Рассмотрим процесс декомпозиции на примере, представленном на рисунке~\ref{figure:decomposition_example} и основанном на небольшой части проекта BusyBox.
Пример иллюстрирует результат работы каждого шага метода.
Прямоугольниками со сплошными границами представлены целевые модули, а нецелевые модули имеют пунктирные границы.
Стрелки соответствуют зависимостям по вызову функций между файлами и модулями.
\begin{itemize}
    \item Пусть после выполнения определения состава программы оказалось, что в программе 5 файлов, зависимости по вызову функций между которыми представлены на рисунке. 
    В данном примере файлы в левой части соответствуют апплетам \textit{bzip2} и \textit{catc}, каждый из которых имеет свою функцию \textit{main}.
    Файл из директории \textit{libbb} соответствует одноименной библиотеке функций, которая может быть использована любым апплетом.
    Файлы из директории \textit{archival/libarchive} реализуют вспомогательные функции для различных апплетов, предназначенных для сжатия и распаковки архивов.
    \item На втором шаге выполняется выделение модулей на основе некоторой стратегии.
    Пусть в данном примере стратегия на основе графа вызова функций предполагает объединение файлов из одной директории, отделяя друг от друга те модули, в которых в каждом есть своя функция \textit{main}.
    \item На третьем шаге выбираются целевые модули.
    В данном случае целевыми являются модули с файлами \textit{bzip2} и \textit{catc}, которые содержат функции \textit{main}.
    \item На предпоследнем шаге выполняется коррекция состава модулей согласно спецификации декомпозиции.
    Предположим, что пользователь указал, что для всех апплетов из \textit{archival} необходимо добавить файлы из\break \textit{archival/libarchive}, которые в свою очередь не нужно выделять в отдельный модуль.
    \item На заключительном этапе на основе графа вызова функций между модулями для сокращения затрат на моделирование окружения выполняется агрегация апплетов со вспомогательной библиотекой \textit{libbb}.
\end{itemize}

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

\section{Метод спецификации моделей окружения}
В данном разделе представлен метод спецификации моделей окружения модулей на основе систем переходов.

\subsection{Промежуточная модель окружения}
После декомпозиции программы требуется для каждого модуля Си-программы подготовить модель окружения, которая состоит из моделей неопределенных функций и моделей сценариев взаимодействия.

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

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

Способ описания промежуточной модели окружения должен удовлетворять ряду требований для удобства применения на практике:
\begin{itemize}
    \item Модели сценариев взаимодействия должны быть описаны отдельно друг от друга.
    \item Модели событий следует описывать на языке программирования Си. 
    Такой подход призван облегчить восприятие моделей пользователем и упростить их трансляцию на язык Си при подготовке финальной модели окружения.
    \item При агрегации нескольких модулей модель окружения в промежуточном представлении для группы модулей должна быть построена как параллельная композиция моделей сценариев, подготовленных для отдельных модулей.
    Каждая модель сценария описывает события взаимодействия, которые происходят в отдельном потоке окружения согласно семантике выполнения многопоточной программы в соответствии со стандартом POSIX.
\end{itemize}

Рассмотрим способ задания промежуточной модели окружения, не опираясь на конкретный синтаксис, который может быть реализован по-разному.
Пусть требуется разработать модель окружения для модуля программы на языке программирования Си с программным интерфейсом $I = <V_p, F_p, R_e, T_e>$, который содержит множества глобальных переменных, функций, макросов и типов, для которых известны сигнатуры, область видимости в файлах программы и файл с объявлением или определением.
Описание программного интерфейса может быть получено из базы сборки программы.

Промежуточную модель окружения данного модуля обозначим как $M$, где:
\[ M = <V_e, F_e, R_e, T_e, E> \]
Здесь $V_e, F_e, R_e, T_e$ --- это множества вспомогательных вспомогательных переменных, функций, макросов и типов.
Для переменных заданы объявления и инициализаторы, а для остальных элементов даны определения на языке программирования Си.
Пересечения перечисленных множеств с соответствующими множествами из $I$ могут быть непустыми.
$E$ содержит конечное множество моделей сценариев взаимодействия модуля программы и окружения.

Множество $F_e$ содержит определения моделей функций из окружения и \textit{служебных функций}.
Множества $R_e, T_e$ и $V_e$ являются вспомогательными и необходимы для реализации моделей функций окружения и моделей сценариев взаимодействия.
Служебные функции выполняют следующие задачи:
\begin{itemize}
    \item При помощи данных функций может быть выделена общая функциональность ряда моделей.
    \item Служебные функции могут реализовывать модели функций стандартной и других библиотек, которые необходимы при использовании определенных инструментов верификации моделей программ.
    К таким функциям относятся функции выделения памяти, работы со строками, механизмами синхронизации и др.
    \item Некоторые служебные функции служат для <<связывания>> моделей окружения и моделей требований. Подробнее этот вопрос рассматривается в разделе, посвященном синтезу моделей требований.
\end{itemize}

Множество моделей сценариев взаимодействия $E$ содержит модели сценариев, которые делятся на два вида: модели функций окружения и модели потоков окружения. 
Каждая модель функции окружения реализует модель сценария взаимодействия, события которого происходят во время выполнения некоторой функции окружения из $F_p \setminus F_e$. 
Модель потока окружения реализует модель сценария, события которого выполняются
в некотором отдельном потоке окружения.
Все модели потоков окружения в точке входа модели окружения начинают выполнение одновременно.

Каждая модель сценария определяется четверкой:
\[ \varepsilon = <\mathcal{V}, \mathcal{A}, \alpha_0 ,\mathcal{R}>\]
Где $\mathcal{V}$ --- это множество переменных состояния, а $\mathcal{A}$ --- это множество \textit{действий} $\mathcal{R}:~ \mathcal{A}~\times~\mathcal{A}$ --- отношение переходов, описывающее допустимый порядок следования действий.

Модель сценария всегда начинается с выполнения действия $\alpha_0$, а последующие действия определяются отношением переходов $\mathcal{R}$. 
Будем различать действия трех видов: \textit{прием} и \textit{отправка} сигналов, а также \textit{модели событий}.

Модели событий предназначены для вызова точек входа и выполнения операций с их параметрами.
Модель события определяется тройкой:
\[\alpha = <\varphi, \beta, \psi> \]
Где $\beta$ --- это базовый блок кода на языке программирования Си, состоящий из операций над переменными $\mathcal{V} \cup V_p \cup V_e$, в котором могут быть вызваны функции из $F_p$ и $F_e$.
Базовый блок должен содержать корректный код и иметь один вход и один выход, то есть, если в блоке есть операторы ветвления или циклов, то они полностью должны входить в состав блока.
В базовых блоках запрещено объявлять новые переменные и использовать оператор $goto$.
Логические выражения $\varphi$ и $\psi$ на языке программирования Си над переменными $\mathcal{V}_i \cup V_p \cup V_e$ описывают предусловия и постусловия действия.

Действия передачи сигналов служат для описания зависимостей по порядку и данным между моделями событий из разных сценариев.
Рассмотрим модель сценария $\varepsilon_i$ с действием отправки сигнала и модель сценария $\varepsilon_j$ с действием получения сигнала.
Соответствующие действия $\alpha_i \in \mathcal{A}_i$ и $\alpha_j \in \mathcal{A}_j$ имеют вид:
\begin{align*}
&\alpha_i = <\varphi_i, \varepsilon_i, l_m>
&\alpha_j = <\varphi_j, \pi_j, l_n, \psi_j>    
\end{align*}
Константы $l_m$ и $l_n$ называются именами сигналов.
Передача сигнала возможна только тогда, когда в соответствующих действиях отправки и получения указано одно и то же имя сигнала $l_m = l_n$.
Логические выражения $\varphi_j$ и $\psi_j$ на языке программирования Си над переменными из $\mathcal{V}_j \cup V_p \cup V_e$ определяют предусловие и постусловие приема сигнала.
Предусловие посылки сигнала является логическим выражением $\varphi_i$, определенным на множестве переменных $\mathcal{V}_i \cup V_p \cup V_e$.
Два набора переменных $\varepsilon_i: {v_1, ..., v_k}$ где $t = 1..k, v_t \in \mathcal{V}_i$ и $\pi_j: {u_1, ..., u_k}$ где $t = 1..k, u_t \in \mathcal{V}_j$ предназначены для передачи значений между переменными состояния отправителя и получателя:
\begin{align*}
&\forall t = 0..k:~v_t := u_t
\end{align*}
Типы переменных должны либо совпадать, либо допускать преобразование.

Посылка сигнала происходит между одним получателем и одним отправителем согласно модели синхронизации потоков рандеву, предложенной в работе~\cite{Hoare:1978:CSP}.
Передача происходит между двумя моделями сценариев, одна из которых отправляет сигнал, а другая получает, причем имя сигнала в заданных действиях должно совпадать.
Для этого получатель должен выполнить действие получения сигнала, разрешенное отношением переходов, а отправитель выполнить соответствующее действие посылки сигнала.
Как только и отправитель, и получатель начали выполнять соответствующие действия, то может быть произведена передача данных.
После передачи данных отправитель может продолжать выполнение других действий, а получатель продолжит свою работу только после получения данных, которое может произойти не одновременно с отправкой.
Отправитель или получатель могут предпринять и другие действия, допустимые отношением переходов, независимо от наличия потенциальных получателей или отправителей.
Если же отношение переходов не разрешает выполнение других действий кроме посылки или отправки сигнала, то никаких действий в модели сценария выполняться не должно до появления необходимой пары для передачи сигнала.
Если потенциальных получателей или отправителей несколько, то пересылка сигнала происходит согласно недетерминированному выбору двух участников, а остальные модели сценариев, которые должны выполнить посылку или отправку сигнала с тем же именем, ожидают завершения передачи сигнала.

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

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

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

\subsection{Пример промежуточной модели окружения}
Рассмотрим пример промежуточной модели окружения для модуля подсистемы.
Для задания моделей сценариев промежуточной модели окружения будем использовать язык Си, в котором будут добавлены расширения для обозначения действий передачи и получения сигналов.
Операции для посылки и приема сигнала $A$ пусть имеют вид $send(A, p1, ..., pN);$ и \break $receive(A, p1, ..., pN);$ соответственно.
Порядок действий будем задавать при помощи условного оператора и функции \textit{\_\_VERIFIER\_nondet\_int}, а предусловия и постусловия будут заданы при помощи функции \textit{\_\_VERIFIER\_assume}.
Такой способ несколько затрудняет восприятие, зато позволяет строго обозначить начало и конец описания каждого действия, которые будем сопровождать соответствующими комментариями.

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

\begin{lstlisting}[language=C,basicstyle=\small]
void init_scenario(void) {
    // State vars
    int ret;

    // Transition Relation    
    // Block Action 1 begin
    ret = tty_init();
    // Block Action 2 end
    if (__VERIFIER_nondet_int()) {
        // Send Action 2 begin
        __VERIFIER_assume(ret == 0);
        send("INITIALIZED");
        // Send Action 2 end
    }
}
\end{lstlisting}

Здесь при помощи комментариев на языке Си обозначены конкретные части описания сценария: переменные состояния, операторы отношения переходов и действия.
Первое действие является блоком кода, в котором выполняется вызов функции инициализации подсистемы.
А второе действие с предусловием, выраженным при помощи вызова функции \textit{\_\_VERIFIER\_assume}, отправляет сигнал для активации сценария вызова библиотечных функций, который в свою очередь может быть задан следующим образом:

\begin{lstlisting}[language=C,basicstyle=\small]
void functions_scenario(void) {
    // State vars
    int ret;
    struct tty_driver *driver;
    struct tty_operations *ops;
    
    // Transition Relation
    // Receive Action 1 begin
    receive("INITIALIZED");
    // Receive Action 1 end
    // Block action 2 begin
    driver = tty_alloc_driver(...)
    // Block action 2 end
    if (__VERIFIER_nondet_int()) {
        // Block action 3 begin
        __VERIFIER_assume(driver != 0);
        ops = __VERIFIER_nondet_pointer();
        tty_set_operations(driver, ops);
        // Block action 3 end
        // Block action 4 begin
        ret = tty_register_driver(driver)
        // Block action 4 end
        if (__VERIFIER_nondet_int()) {
            // Send Action 5 begin
            __VERIFIER_assume(ret == 0);
            send("Register TTY callbacks", driver);
            // Send Action 5 end
            // Receive Action 6 begin
            receive("Unregister TTY callbacks", driver);
            __VERIFIER_assume(driver->ops == ops);
            // Receive Action 6 end
            // Block action 7 begin
            tty_unregister_driver(driver);    
            put_tty_driver(driver);
            // Block action 7 end
        } else {
            // Block action 8 begin
            __VERIFIER_assume(ret != 0);
            // Block action 8 end
        }
    }    
}
\end{lstlisting}

Первым действием сценария является прием сигнала, который означает, что подсистема инициализирована.
Затем выполняется вызов точек функций подсистемы.
Отличительной особенностью данной модели по сравнению с моделью окружения на языке Си, которая была предложена в первом разделе данной главы, является посылка и ожидание сигналов \textit{Register TTY callbacks} и \textit{Unregister TTY callbacks} после успешного вызова функции \textit{tty\_register\_driver}.
Данные действия указаны для демонстрации того, как указание о возможности вызова обработчиков драйверов может быть передано соответствующим моделям сценариев.
Данная модель сценария ожидает сигнал \textit{Unregister TTY callbacks}, который означает, что вызов обработчиков драйверов завершен.
Если в промежуточной модели окружения нет моделей сценариев, которые отправляют или принимают сигналы \textit{Register TTY callbacks} и \textit{Unregister TTY callbacks}, то они могут быть удалены из рассматриваемой модели вызова библиотечных функций при трансляции на язык Си.

\subsection{Трансляция промежуточных моделей окружения}
\input{2-formal}

\section{Метод синтеза моделей окружения}

В данном разделе представлен метод автоматизированного синтеза моделей окружения для модулей программ на языке программирования Си.

Синтез моделей окружения для модулей Си-программ выполняется \textit{генератором моделей окружения} на основе описания программного интерфейса модулей и спецификаций предположений об окружении согласно схеме, изображенной на рисунке~\ref{figure:em}.
Генератор моделей окружения в качестве входных данных получает спецификации предположений об окружении, разработанные вручную, модуль программы и описание его программного интерфейса, которое является частью базы сборки программной системы.
В качестве выходных данных генератор синтезирует модель окружения на языке программирования Си.
Процесс синтеза состоит из двух шагов:
\begin{enumerate}
    \item На первом шаге \textit{построители моделей сценариев} независимо друг от друга синтезируют модели сценариев, которые формируют промежуточную модель окружения.
    \item На втором шаге промежуточная модель окружения при помощи \textit{транслятора} переводится на языке программирования Си для получения финальной модели окружения.
\end{enumerate}

\begin{figure}
\centering
\includegraphics[scale=1.2]{generators}
\caption{Схема синтеза моделей окружения.}
\label{figure:em}
\end{figure}

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

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

Рассмотрим пример работы простейшего построителя моделей сценариев для вызова функций по заданному пользователем списку имен.
Такой компонент выполняет следующие шаги:
\begin{enumerate}
    \item В качестве спецификации предположений об окружении пользователь передает список имен функций или шаблон, заданный при помощи регулярного выражения, и конфигурационные параметры, определяющие требуется ли вызывать функции в цикле.
    \item Построитель определяет на основе описания программного интерфейса конкретные функции, которые являются точками входа модуля программы и имена которых входят в список, заданный пользователем.
    Затем из описания программного интерфейса получаются сигнатуры точек входа.
    \item Для каждой функции выполняется генерация функции-обертки, помещаемой в тот файл, где определена точка входа. 
    Такая функция-обертка содержит инициализацию параметров с использованием вспомогательных функций для моделирования неопределенных значений, а также сам вызов целевой функции с данными параметрами.
    Обертка позволяет избежать ошибок, связанных с областью видимости типов, которые могут использоваться при задании сигнатуры аргументов точки входа, которую требуется вызвать.
    \item Построитель генерирует одну модель сценария для промежуточной модели окружения, которая вызывает точки входа. 
    Каждое действие модели сценария вызывает одну конкретную функцию-обертку.
    \item Отношение переходов, определяющее последовательность действий, зависит от конфигурационных параметров построителя.
    Если отношение переходов должно быть описано на языке программирования Си, тогда может использоваться оператор switch или цикл, в теле которого находится тот же оператор.
    Оператор switch в случайном порядке выполняет одно из действий --- вызов какой-либо функции-обертки.
    \item Все вспомогательные функции и модель сценария передаются транслятору.
\end{enumerate}

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

Транслятор должен иметь ряд конфигурационных параметров, позволяющих настраивать вид модели окружения в зависимости от используемого инструмента верификации моделей программ или проверяемого требования.
На практике может возникать необходимость в следующих преобразованиях:
\begin{itemize}
    \item Выполнять трансляцию промежуточной модели окружения в последовательный или параллельный код на языке программирования Си. 
    При трансляции в последовательный код может требоваться подготовка модели окружения с разной степенью полноты с точки зрения всевозможных чередований событий из разных сценариев.
    \item Для задания параллельной модели окружения могут использоваться разные интерфейсы управления потоками или процессами.
    \item В модели окружения могут быть использованы разные наборы служебных функций.
\end{itemize}

В процессе своей работы транслятор выполняет следующие операции:
\begin{itemize}
    \item Объединяет полученные от построителей сценариев фрагменты промежуточной модели окружения на языке программирования Си, которые обозначались как $V_e, F_e, R_e, T_e$.
    \item Генерирует точку входа, которая вызывает служебную функцию инициализации модели требования.
    Затем в точке входа создаются потоки для сценариев, которые относятся к виду моделей потоков окружения.
    Для этого либо генерируется соответствующий код с созданием и ожиданием POSIX потоков, либо выполняется генерация последовательного кода с некоторым чередованием действий из разных сценариев.
    После завершения всех моделей сценариев в точке входа вызывается служебная функция завершения работы, определение которой находится в модели требования.
    \item Выполняет генерацию вспомогательного исходного кода для трансляции операций посылки и получения сигналов на язык программирования Си, например, в соответствие со схемой, предложенной при доказательстве теоремы об изоморфизме.
\end{itemize}

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

\section{Синтез моделей требований}

Для синтеза моделей требований предлагается использовать метод, предложенный ранее в работе~\cite{NovikovDis}.
Данный метод применялся в системе верификации LDV~Tools и показал возможность успешного применения на практике для проверки различных требований к драйверам операционной системы Linux~\cite{Zakharov2015, configurable:Trudy}.
Хотя в упомянутых работах метод применяется только для спецификации требований корректного использования интерфейса ядра в драйверах, он может быть использован и для других требований и программных систем.

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

Для генерации модели требования используется инструмент CIF для реализации подхода аспетно-ориентированного программирования, предложенного Е.~М.~Новиковым и апробированным при верификации драйверов ОС Linux в рамках системы верификации LDV~Tools~\cite{Novikov2013}.
Спецификация требования подается инструменту CIF вместе с исходным кодом модуля программы.
Инструмент выполняет препроцессирование исходного кода модуля и его инструментацию для синтеза модели требования на основе спецификации требования и добавления ее в исходный код модуля.

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

\section{Компоновка верификационных задач}
В качестве входных данных при компоновке верификационных задач выступают файлы с исходным кодом программы, файлы моделей окружения и требования, а также конфигурационные параметры, заданные пользователем.
В качестве результата компоновки из входных данных должна быть получена отдельная верификационная задача в формате, предложенном сообществом SV"~COMP.

Как ранее упоминалось, для получения исходного кода верификационной задачи может потребоваться инструментация исходного кода.
Для возможности применения данного метода модели должны быть сгенерированы в соответствующих форматах.
После или в процессе выполнения инструментации также следует препроцессировать исходный код всех файлов на языке программирования Си.
Некоторые инстрменты верификации моделей программ требуют, чтобы верификационная задача содержала только один файл.
В этом случае можно следует использовать инструменты для объединения файлов, например CIL~\cite{CIL}.

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

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