Software & Systems

В последнее время широкое распространение в области верификации получил метод Model Checking [1–6], или метод проверки на моделях. Суть его – в верификации свойств системы, представленных в виде формул временных логик LTL или CTL [7, 8]. При этом верифицируемая модель может быть задана явно (путем перечисления всех состояний и соединяющих их ребер) или неявно (путем задания булевых функций, определяющих отношение переходов и множество начальных состояний). Однако при верификации больших информационных систем, в том числе и распределенных программных, зачастую приходится иметь дело с очень большим числом состояний вычислительного процесса для их моделей. Например, для программы, в рамках которой одновременно выполняются 10 потоков, причем каждый из них может находиться в одном из 5 состояний, общее число состояний вычислительного процесса может достигать 510 = 9765625, что может стать непреодолимым препятствиям на пути верификации тех или иных ее свойств. Кроме того, в модели могут явно присутствовать вычисления, переход в которые никогда не встретится на практике.

Сегодня существуют два основных подхода к выполнению верификации данных систем:

−      построение более абстрактной, менее детализированной модели на базе исходной;

−      выполнение верификации модели на ее сжатом, приведенном к некоторому сжатому виду представлении.

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

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

Ограничение верифицируемых моделей

Рассмотрим предлагаемый метод ограничения верифицируемых моделей на примере работы кухонной микроволновой печи. Через c, m, w, f обозначим предикаты, определяющие состояния нашей модели: с – дверца печи закрыта, m – задан режим работы печи, w – печь работает, f – в печи присутствует еда. На рисунке 1 изображена модель печи, представленная в виде структуры Крипке.

Для наложения ограничений необходимо преобразовать данную модель к автомату Бюхи [9], который представлен на рисунке 2.

Ограничением, накладываемым на эту модель, будет следующее условие: при работе с печью в ней обязательно должна находиться еда или печью никто не пользуется. Представим это ограничение в виде формулы временной логики LTL: φ = G(f Ú Æ) – «Всегда либо в печи присутствует еда, либо дверца открыта, режим не задан, печь не работает и еда в печи отсутствует»; Æ ≡ ˥c Ù ˥m Ù ˥w Ù ˥f. Для использования данного высказывания в качестве ограничивающего условия необходимо также преобразовать его в автомат Бюхи. Через S обозначим входной алфавит этого автомата над множеством 2AP, где S={Æ, {c}, {m}, {w}, {f}, {c, m}, {c, w}, …, {c, m, w, f}}, AP={c, m, w, f} [1]. Результат представлен на рисунке 3.

Двойной окружностью в автоматах Бюхи обозначается допускающее состояние, то есть такое состояние, через которое автомат должен будет проходить бесконечное число раз, а одинарной окружностью обозначаются недопускающие состояния, то есть такие состояния, пребывание автомата в которых бесконечно долго свидетельствует о недопустимости входного слова w [1].

Построив синхронную композицию автоматов Bm и Bφ в соответствии с описанным в [1] методом, получим автомат Бюхи BmÄBφ, в котором будет соблюдаться заданное нами условие. На рисунке 4 представлена соответствующая синхронная композиция автоматов Бюхи.

В качестве результирующего автомата, удовлетворяющего заданному ограничению, для которого будет выполняться верификация проверяемых свойств, примем автомат Бюхи R(BmÄBφ), где R – функция редукции, исключающая сначала все изолированные и недопускающие состояния, а затем все допускающие состояния, из которых не существует ни одного перехода. Изолированными будем называть такие состояния, в которые не существует ни одного пути из начального состояния. На рисунке 5 изображен данный автомат.

Как видно из рисунка 5, область вычислений нашей модели сократилась на четыре состояния по сравнению с исходной (рис. 2).

Теперь проверим, возможна ли работа печи с открытой дверцей. Для проверки данного свойства введем следующую формулу временной логики LTL: φ1 = G(w ® c) – «Всегда, если печь работает, то значит, дверца закрыта». Возьмем отрицание данной формулы ˥φ1 = ˥(G(w ® c)) = F(w Ù ˥c) и построим для нее соответствующий автомат Бюхи (рис. 6).

Этот автомат переходит в допускающее состояние только в случае возникновении ошибки, то есть тогда, когда микроволновая печь будет работать с открытой дверцей. Таким образом, построив синхронную композицию данного автомата и проверяемого, можно установить, способна ли система перейти в ошибочное состояние и, если да, то в каком случае. Композиция автоматов R(Bm⊗Bφ) и B(˥φ1) представлена на рисунке 7.

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

Ограничение моделей распределенных программных систем

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

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

Введем для рассматриваемой системы ограничение «Всегда осуществляется запись» с целью оставить лишь потоки «писателей», так как только они способны забрать ресурс в бессрочное пользование в рамках заданных нами условий. Представим это ограничение в виде формулы временной логики LTL: φ = G(W1 Ú W2 Ú W3) и построим для нее соответствующий автомат Бюхи (рис. 10).

В этом случае входной алфавит Ʃ данного автомата над множеством 2AP примет вид: S={Æ, {W1}, {W2}, {W3}, {R1}, {R2}, {W1, W2}, …, {W1, W2, W3, R1, R2}}, AP={W1, W2, W3, R1, R2}.

Синхронная композиция автоматов BmÄBφ, отвечающая заданному нами условию, представлена на рисунке 11.

Окончательный результат ограничения нашей модели после применения функции редукции R к композиции BmÄBφ можно видеть на рисунке 12.

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

Как видно из этого рисунка, данный автомат перейдет в допускающее состояние только в том случае, если существует переход, помеченный {Wi}, и допускающее состояние всегда будет переходить само в себя только по переходу, помеченному тем же {Wi}. Композиция автоматов R(BmÄBφ) и B(˥φ1) представлена на рисунке 14.

В этой композиции существует переход в допускающее состояние (S1, 2), что свидетельствует о том, что формула ˥φ1 выполняется и в системе может возникнуть тупиковая ситуация в случае работы первого «писателя». Из состояний (S2, 1) и (S3, 1) нет переходов в допускающие, так как, если, например, перейти по переходу {W2} из состояния (S2, 1) в (S2, 2), то в соответствии с контрольным автоматом на рисунке 13 был бы возможен переход дальше только по переходам, помеченным {W2}. Однако из состояния (S2, 2) существует переход, например, в (S3, 2), из которого, в свою очередь, существует переход, помеченный {W3}, что явно противоречит контрольному автомату.

  Эффективность метода ограничения моделей

В общем виде работу метода ограничения верифицируемых моделей можно описать следующим образом. По заданной модели M строится автомат Бюхи Bm, допускающий все вычислительные последовательности, которые возможны в M. По заданной LTL-формуле j строится ограничивающий автомат Бюхи, допускающий лишь те вычислительные последовательности, на которых выполняется j. После этого строится синхронная композиция автоматов BmÄBφ, на которой после применения к ней редуцирующей функции R осуществляется последующая верификация требуемых свойств по алгоритму, описанному в [1].

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

Пусть дана модель некоторой системы M(n), где n – число ее состояний для автомата Бюхи. И пусть также дано некоторое множество проверяемых условий Ψ{S1(k1), S2(k2), …, Sm(km)}, где Si(ki) – контрольный автомат проверяемого условия от ki состояний автомата Бюхи. Для выполнения проверки очередного условия на моде- ли требуется построить синхронную композицию контрольного автомата проверяемого условия и автомата имеющейся модели, как описано в [1, 10]. Таким образом, для проверки всего множества условий Ψ на модели M потребуется построить m композиций: M×S1 & M×S2 & … & M×Sm. Суммарное число операций данного процесса будет равно op = nk1 + nk2 + … + nkm = S(1≤i≤m) (n ki) = = nS (1≤i≤m) ki. Теперь введем модель M’(n’), которая является сокращенной версией модели M(n) после применения к ней функции редукции R и удовлетворяет условию n’

Покажем, что существует такая ситуация, когда имеет место неравенство op’+r

Проверим эффективность метода для вышеописанного примера с микроволновой печью. Исходное число состояний модели n=10 (рис. 2), число состояний модели после ограничения n’=6 (рис. 5). Число состояний усекающего условия z=2 (рис. 3), суммарное число состояний всех контрольных автоматов m=2 (рис. 6). Таким образом, ускорение A=1/(6/10 + 2/2) = 0,625, что свидетельствует о неэффективности применения данного метода в конкретном случае. Однако попробуем ввести еще 2 некоторых дополнительных условия проверки для этой системы, к примеру: «готовка когда-нибудь начнется» и «после закрытия дверцы задается режим готовки». Контрольные автоматы Бюхи для этих дополнительных условий будут состоять из 2 состояний каждый, и, таким образом, в конечном итоге при введении этих 2 допол- нительных условий μ = 6, а итоговое ускорение A=1/(6/10 + 2/6) = 1,07143.

Поскольку ускорение в 0,07 не является показательным, возьмем некоторую абстрактную ситуацию. Пусть дана некоторая модель, состоящая из 1012 состояний. После применения к ней данного метода она сократилась до 1010 состояний. В качестве проверяемых условий будут даны 4 условия, описанные в [1]: свойства достижимости, безопасности, живости и справедливости. Суммарное число всех состояний автоматов Бюхи для этих свойств будет равно 8. Усекающий автомат будет состоять из 2 состояний. Таким образом, получится следующее ускорение: A=1/(1010/1012 + + 2/8) = 3,846. Если же проверяемых условий будет хотя бы 10, а суммарное число состояний всех автоматов Бюхи будет равно 20, получим следующее ускорение: A=1/(1010/1012 + 2/20) = 9,(09).

В таблице приведена зависимость ускорения A от значений n’/n и z/m.

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

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

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

Литература

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

2.     Суад Алагич, Майкл Арбиб. Проектирование корректных структурированных программ. М.: Радио и связь, 1979. 292 с.

3.     Кораблин Ю.П., Косакян М.Л. Анализ моделей программ на языке асинхронных функциональных схем средствами темпоральной логики линейного времени // Программные продукты и системы. 2014. № 2 (106). С. 5–10.

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

5.     Ábrahám E., Havelund K. (Eds). Tools and Algorithms for the Construction and Analysis of Systems. Springer; 2014 edition (March 24, 2014), 652 p.

6.     Bérard B., Bidoit M., Finkel A., Laroussinie F., Petit A., Petrucci L., Schnoebelen P. Systems and Software Verification. Model Checking Techniques and Tools. Springer, 2001, 190 p.

7.     Kröger, Fred, Merz, Stephan. Temporal Logic and State Systems. Springer; 2008 ed. (March 27, 2008), 436 p.

8.     Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification, 1992 edition (December 18, 1991), 427 p.

9.     Khoussainov B., Nerode A. Automata Theory and its Applications. Boston–Basel–Berlin, Birkhäuser Publ., 2001, 432 p.

10.  Велдер С.А., Лукин М.А., Шалуто А.А., Яминов Б.Р. Верификация автоматных программ. СПб: Наука, 2011. 244 с.