Программные продукты и системы

Верификация работы программных и технических систем является неотъемлемой частью их жизненного цикла. Существует целый ряд инструментов и средств верификации, которые являются более удобными и эффективными при тех или иных условиях, на тех или иных этапах проектирования и сопровождения. Однако за последние два десятилетия лучше всего себя зарекомендовали инструменты формальной верификации, работа которых может быть автоматизирована, а корректность функционирования – доказана формально. Наиболее активно используемым инструментом на сегодняшний день является метод формальной верификации на моделях, или Model Checking [1, 2].

Технология процесса верификации програм- мных и технических систем методом проверки на моделях подразумевает создание моделей систем, свойства которых требуется проверить. Так, например, модель системы может быть задана с помощью различных структур данных, в частности таких, как структура Крипке, язык асинхронных процессов Promela, в виде конечного автомата и т.д. Однако независимо от представления модели системы и верифицируемых свойств, заданных на базе логики линейного времени (LTL) [3, 4], необходим, как правило, процесс их преобразования к автоматам Бюхи. При этом алгоритмы преобразования формул LTL в автоматы Бюхи являются нетривиальными, а принципы их функционирования непонятны на интуитивном уровне.

В данной статье рассматривается новая нотация RLTL (recursive linear temporal logic) для представления формул LTL в виде системы рекурсивных уравнений с целью расширения ее описательной мощности [5]. Кроме того, RLTL может быть использована и для задания моделей верифицируемых систем, что предоставляет следующие важные преимущества:

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

-     возможность быстрого и интуитивно понятного преобразования RLTL-структур в автоматы Бюхи для их последующей верификации;

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

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

RLTL-нотация

Рассмотрим рекурсивные представления основных базовых операторов LTL (табл. 1).

Символом ∘ обозначен оператор продолжения (конкатенация выражений), что позволяет использовать оператор X в неявном виде, а также упростить его восприятие, в частности, запись φ1 ∘ φ2 будет пониматься как «φ2 следует за φ1». Под символом ∆, далее именуемым предикатом неопреде- ленности, будем понимать некоторое неопределенное подмножество символов входного алфавита. Под отрицанием предиката неопределенности будем понимать некоторое другое неопределенное подмножество символов алфавита, а под отрицанием отрицания – некоторое третье неопределенное подмножество. Таким образом, отрицание предиката неопределенности является неполным, а каждое последующее отрицание дает неопределенное подмножество символов. Каждое из этих подмножеств ввиду своей неопределенности также может быть обозначено через ∆.

Таблица 1

Рекурсивные представления операторов LTL

Table 1

Recursive presentations of LTL operators

В таблице 1 представлены почти все операторы, используемые в LTL, кроме оператора Xφ, у которого отсутствует рекурсивная форма. Таким образом, поскольку все основные операторы LTL могут быть представлены в рекурсивной форме, авторы полагают, что приведение их к некоторому унифицированному виду, который, следуя [5], будем именовать эквациональной характеристикой, позволит существенно расширить описательную способность LTL и упростит процесс верификации ее формул.

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

Таблица 2

Сочетания операторов LTL в эквациональной форме

Table 2

Equational combinations of LTL operators

Сформулируем основные аксиомы логики RLTL:

Построение RLTL-моделей

Структуры на базе RLTL-нотации могут быть интерпретированы в качестве недетерминированного конечного автомата, который на вход получает бесконечные цепочки и моделирует поведение реагирующих систем. Так, рассмотрим формальное определение автомата Бюхи. Автомат Бюхи – это пятерка (S, Σ, S0, δ, F), где Σ – конечное множество символов (алфавит); S – множество состояний; S0 ⊆ S – множество начальных состояний (содержащее только один элемент для детерминированного случая); δ: S × Σ→2s – отношение переходов (для детерминированного автомата δ: S × Σ→S); F ⊆ S – множество допускающих (финальных) состояний.

Нетрудно убедиться, что любая структура на базе RLTL-нотации может быть интерпретирована в качестве автомата Бюхи в соответствии с данным определением. В качестве алфавита в RLTL также выступает некоторое множество символов Σ. В качестве состояний выступает множество метапеременных S = {F1, F2, …, Fn}, задающих уравнения системы. По умолчанию в качестве начального состояния выступает метапеременная первого уравнения системы, однако, если существует несколько начальных состояний, их можно задать в виде элементов соответствующего множества. Функция переходов для RLTL остается аналогичной автоматам Бюхи, где в роли переходов выступает оператор продолжения ∘, за которым следует метапеременная, обозначающая состояние, в которое осуществляется переход. Что касается множества допустимых или финальных состояний, то в RLTL не существует аналога, поэтому необходимо явное задание множества соответствующих метапеременных.

Для задания с помощью RLTL-нотации моделей систем достаточно использовать лишь тройку значений (S, Σ, δ), поскольку каждое состояние модели системы является допустимым, а любое множество начальных состояний из более чем одного элемента может быть заменено единственным начальным состоянием, из которого существуют переходы по любому из символов алфавита в каждое из этих состояний. В качестве примера зададим в терминах RLTL простую модель работы светофора на основе ее устного описания: «Горит зеленый сигнал, затем загорается желтый, а после желтого – красный. После красного сигнала снова загорается желтый, за ним зеленый. В такой последовательности сигналы продолжают чередоваться дальше». Опишем модель работы светофора следующей тройкой значений (S, Σ, δ): S = {F1, F2, F3, F4}, Σ = {g, y, r}, δ = {g: F1→F2, y: F2→F3, r: F3→F4, y: F4→F1}, где g – зеленый сигнал светофора; y – жел- тый сигнал; r – красный сигнал. В RLTL-нотации модель будет иметь следующий вид: F1 = g ∘ F2, F2 = y ∘ F3, F3 = r ∘ F4, F4 = y ∘ F1.

Использование пятерки значений (S, Σ, S0, δ, F) требуется лишь в тех случаях, когда необходимо превратить данные на базе RLTL в автомат Бюхи. Так, пусть дана формула LTL GFφ – «всегда в будущем будет наступать φ». В терминах RLTL-нотации она будет выглядеть следующим образом: F1 = φ ∘ F1 ∨ ∆ ∘ F2, F2 = φ ∘ F1 ∨ ∆ ∘ F2.

В данном случае система задана тройкой значений (S, Σ, δ), где S = {F1, F2}, Σ = {φ}, δ = {φ: F1→F1, φ: F2→F1, ∆: F1→F2, ∆: F2→F2}. Для превращения данной формулы в автомат Бюхи достаточно указать множество начальных и множество допустимых состояний: S0 = {F1} и F = {F1}. Аналогично может быть задана и модель любой системы на базе RLTL.

Таким образом, любая RLTL-структура, использующая тройку значений (S, Σ, δ), может быть превращена в автомат Бюхи за счет задания множеств начальных и допустимых состояний. Возможность простого и интуитивно понятного превращения формул RLTL в автоматы Бюхи и наоборот, как и представленные выше примеры, подтверждает возможность задания моделей верифицируемых систем сразу на базе RLTL. Сам процесс задания моделей систем может быть выполнен двумя способами:

-     построение модели системы на базе структуры Крипке с ее последующим преобразованием в RLTL; поскольку структуры Крипке могут быть быстро преобразованы в автоматы Бюхи [1], их преобразование в RLTL-формулы также выполняется относительно просто;

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

Абстракция и унификация RLTL-моделей

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

-     редукция частичных порядков [6];

-     абстракция данных [6];

-     хэширование битовых состояний (вместо полных состояний хранится лишь их хэш, что снижает требования к объему памяти, но уменьшает полноту системы) [7];

-     ускорение проверки «корректности в слабом смысле», или Weak Fairness [8].

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

Для упрощения моделей систем введем операции абстракции и унификации. Операция абстрак- ции позволяет осуществлять сокращение числа свойств моделей систем, а операция унификации – объединение однотипных элементов. Операцию абстракции обозначим как ABS, где H – множество заменяемых символов; α – заменяющий символ (тот символ, на который заменяются элементы из множества H); φ – атомарный предикат (символ алфавита); μi – формула. Аксиомы, описывающие свойства данной операции, представлены далее:

Операция унификации базируется на четырех основных правилах:

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

В качестве примера возьмем некоторый вариант модели алгоритма «читатели-писатели» для трех «писателей» и двух «читателей». Модель соответствующей системы представлена в виде структуры Крипке на рисунке.

Сформулируем модель данной системы в терминах RLTL-нотации. Каждому состоянию модели Крипке будет сопоставлена своя метапеременная, определяющая соответствующее уравнение системы. В качестве алфавита будет выступать Σ = {W1, W2, W3, R1, R2, R12}. Переходы, ведущие из конкретного состояния, будут помечены символом этого состояния. Поскольку первое состояние си- стемы не помечено ни одним символом, в RLTL все переходы из данного состояния будут помечены символом неопределенности, или ∆.

FM = ∆ ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FW1 = W1 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FW2 = W2 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FW3 = W3 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FR1 = R1 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FR2 = R2 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FR12 = R12 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

Важно учитывать, относительно чего плани- руется производить упрощение системы. Так, в данном случае пусть проверка системы будет выполняться относительно следующего условия, заданного в терминах LTL: φ = GF(˥Wi) – «Всегда в будущем процесс записи для любого из «писателей» будет обязательно завершен». Как видно из формулы, в процессе верификации не будет анализироваться ни один из «читателей», так как в формуле не участвуют предикаты R1 и R2. В связи с этим можно выполнить абстракцию модели системы относительно всех «читателей».

Применим представленные аксиомы к описанному выше примеру. Поскольку абстракция в этом случае выполняется относительно предикатов R1 и R2, H = {R1, R2, R12}, а в качестве символа замены будет использован некоторый символ, например α = R. Таким образом, получим:

ABS(FM) = FM = =ABS(∆ ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12))

ABS(FW1) = FW1 = =ABS(W1 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12))

ABS(FW2) = FW2 = =ABS(W2 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12))

ABS(FW3) = FW3 = =ABS(W3 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12))

ABS(FR1) = FR1 = =ABS(R1 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12))

ABS(FR2) = FR2 = =ABS(R2 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12))

ABS(FR12) = FR12 = =ABS(R12 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12))

После применения аксиом AB1–AB5 система уравнений примет следующий вид:

FM = ∆ ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FW1 = W1 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FW2 = W2 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FW3 = W3 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FR1 = R ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FR2 = R ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FR12 = R ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

Применение представленных выше аксиом позволило сократить общее число символов алфавита (предикатов) системы, однако число ее состояний и переходов осталось прежним. Правило UN1 позволяет сократить число состояний модели верифицируемой системы путем унификации однотипных элементов вычислительного пути. Применим данное правило к системе, полученной на предыдущем шаге, где N = {R1, R2, R12}:

FM = ∆ ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FW1 = W1 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FW2 = W2 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FW3 = W3 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

FN = R ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FR1 ∨ FR2 ∨ FR12)

Применение правил UN2–UN4 позволяет унифицировать однотипные переходы RLTL-модели. После применения данных правил модель примет вид:

FM = ∆ ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FN ∨ FN ∨ FN)

FW1 = W1 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FN ∨ FN ∨ FN)

FW2 = W2 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FN ∨ FN ∨ FN)

FW3 = W3 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FN ∨ FN ∨ FN)

FN = R ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FN ∨ FN ∨ FN)

Выполнив правило дизъюнкции, получим упрощенную модель системы «читатели-писатели»:

FM = ∆ ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FN)

FW1 = W1 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FN)

FW2 = W2 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FN)

FW3 = W3 ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FN)

FN = R ∘ (FW1 ∨ FW2 ∨ FW3 ∨ FN)

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

Приведем также пример упрощения модели светофора, описанной ранее в терминах RLTL. Пусть проверка этой системы будет выполняться относительно следующего условия, заданного в терминах LTL: φ = GF(g) – «Всегда в будущем будет загораться зеленый сигнал светофора». Тогда в качестве множества заменяемых символов можно взять N = {y, r}, а в качестве символа замены используем просто символ s, который будет означать stop, α = s. Таким образом, получим:

ABS(F1) = ABS(g ∘ F2)

ABS(F2) = ABS(y ∘ F3)

ABS(F3) = ABS(r ∘ F4)

ABS(F4) = ABS(y ∘ F1)

После применения аксиом AB1–AB5 система уравнений примет следующий вид:

F1 = g ∘ F2

F2 = s ∘ F3

F3 = s ∘ F4

F4 = s ∘ F1

Для сокращения числа состояний системы применим к ней правило UN1, где N = {2, 3, 4}, и получим: F1 = g ∘ F2, FN = s ∘ F1.

И наконец, применив правила UN2–UN4, получим сокращенную модель светофора: F1 = g ∘ FN, FN = s ∘ F1.

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

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

1.    Построить модель для каждого драйвера (подпрограммы) на базе RLTL.

2.    Построить верифицируемые свойства на базе RLTL.

3.    Для каждой модели выполнить операцию абстракции:

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

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

-     выполнить абстракцию с помощью аксиом AB1–AB5.

4.    Для каждой модели выполнить операцию унификации с помощью аксиом UN1–UN4.

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

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

Заключение

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

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

Литература

1.     Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб: БХВ-Петербург, 2010. 552 с.

2.     Кораблин Ю.П. Семантика языков распределенного программирования. М.: Изд-во МЭИ, 1996. 102 с.

3.     Kroger F., Merz S. Temporal Logic and State Systems. Springer, 2008, 436 p.

4.     Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, NY, 1992, 427 p.

5.     Шипов А.А., Кораблин Ю.П. Эквациональная характеристика формул LTL // Программные продукты и системы. 2015. № 4. С. 175–179.

6.     Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking; [пер. с англ.]. М.: Изд-во МЦНМО, 2002. 416 с.

7.     Holzman G.J. An Analysis of Bitstate Hashing. Proc. 15th Int. Conf. on Protocol Specification, Testing, and Verification, 1998, pp. 301–314.

8.     Olderog E.-R., Apt K.R. Fairness in Parallel Programs: The Transformational Approach. ACM Transactions on Programming Languages and Systems, July 1988, vol. 10, no. 3, pp. 420–455.