Верификация спецификаций в языке L относительно темпоральных свойств, не выразимых в этом языке

Размещено на http://www.allbest.ru

Размещено на http://www.allbest.ru

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

В настоящей работе предполагается, что для спецификации автоматов используется достаточно простой логический язык L [1]. Простота этого языка обусловлена необходимостью иметь эффективные процедуры синтеза императивного представления алгоритма, исходя из его декларативной спецификации. В качестве языков для описания проверяемых свойств широко применяются темпоральные логики. В этом случае для верификации наибольшее распространение получил теоретико-автоматный подход, при котором осуществляется проверка на пустоту языка, представимого произведением автоматных моделей для верифицируемого алгоритма и отрицания формулы, выражающей необходимое свойство. Недостатком такого подхода является высокая сложность используемых процедур, ограничивающая область его применения. В статье рассматриваются свойства, представимые формулами из несколько расширенного класса GR(1) [2] темпоральной логики с линейным временем LTL [3]. Для этого случая предлагается более простой подход к верификации темпоральных свойств алгоритма, не требующий построения автоматных моделей. Хотя рассматриваемые свойства не выразимы в языке L, предлагаемый подход ограничивается эффективными средствами проверки непротиворечивости формул языка L [4, 5].

ЯЗЫК L СПЕЦИФИКАЦИИ РЕАКТИВНЫХ АЛГОРИТМОВ.

Спецификация в языке L имеет вид формулы tF(t), интерпретируемой на множестве Z целых чисел. Формула F(t) строится с помощью логических связок из атомарных формул (атомов) вида p(t - k), где p -- одноместный предикатный символ, t -- переменная, принимающая значения из множества целых чисел, рассматриваемого как множество моментов дискретного времени, а k -- натуральное число, называемое рангом атома. Разность между максимальным и минимальным значениями рангов атомов, встречающихся в формуле, называется ее глубиной.

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

Пусть -- конечный алфавит, Z -- множество целых чисел, а N+ = {z Z z 0}. Отображения u: Z и l: N+ называются соответственно двусторонним сверхсловом (обозначается …u(2)u(1)u(0)u(1)u(2)…) и сверхсловом (обозначается l(1)l(2)… ) в алфавите . Отрезок u()u(+1)…u(+k) двустороннего сверхслова u обозначается u(, +k). Бесконечный отрезок u(k+1, ) назовем k-суффиксом двустороннего сверхслова u. Если значение k не существенно, то будем говорить об -суффиксе. Множество всех сверхслов в алфавите обозначается , а двустороннее сверхслово (сверхслово), представляющее собой бесконечное повторение одного и того же непустого слова r, обозначим rZ (r).

Каждой формуле F = tF(t) языка L ставится в соответствие множество всех моделей для этой формулы, т.е. множество таких интерпретаций, на которых F истинна. Пусть = {p1, …, pm} -- множество всех предикатных символов, встречающихся в формуле F (сигнатура формулы F). Интерпретация формулы F -- это упорядоченный набор определенных на Z одноместных предикатов 1 m, соответствующих предикатным символам из . Пусть -- множество всех двоичных векторов длины m, тогда интерпретацию I = <1 m> можно представить в виде двустороннего сверхслова в алфавите , а множество всех моделей для F -- в виде множества M(F) двусторонних сверхслов в этом алфавите. В дальнейшем не будем различать интерпретации и соответствующие им двусторонние сверхслова, поэтому будем говорить об истинности формулы F на двустороннем сверхслове u Z и значении формулы F(t) в некоторой позиции двустороннего сверхслова u, понимая под этим значение формулы F() в интерпретации u. Сверхсловарная семантика формулы F = tF(t) определяется множеством сверхслов W(F), представляющим собой множество всех -суффиксов двусторонних сверхслов из M(F).

При интерпретации формул вида tFt на множестве целых чисел для любого k Z справедлива эквивалентность tFt tFt+k, где Ft+k обозначает формулу, полученную из Ft путем добавления k к рангам всех ее атомов (сдвиг на k). Таким образом, можно ограничиться рассмотрением формул, у которых максимальный ранг атомов равен 0. Такие формулы будем называть нормализованными вправо. Смысл понятия глубины формулы состоит в том, что истинностное значение нормализованной вправо формулы F(t) глубины r в позиции интерпретации u определяется отрезком u(-r, ) соответствующего двустороннего сверхслова u.

СПОСОБЫ ПРОВЕРКИ НЕПРОТИВОРЕЧИВОСТИ СПЕЦИФИКАЦИЙ В ЯЗЫКЕ L

Для описания рассматриваемых здесь способов проверки непротиворечивости формулы tF(t) языка L удобно воспользоваться понятием пространства состояний, ассоциируемого с этой формулой [4]. Пусть -- сигнатура формулы Ft, а r -- ее глубина. Последовательность s0, s1, …, sr векторов из () назовем состоянием глубины r, а множество Q(r, ) всех таких последовательностей -- пространством состояний глубины r для формулы Ft. На множестве Q(r, ) определим отношение N непосредственного следования так, что за каждым состоянием q = s0, s1, …, sr непосредственно следуют 2|| состояний вида s1, …, sr, s, где s (). Отношение, обратное N, обозначим P и будем называть отношением непосредственного предшествования. Очевидно, что состоянию s0, s1, …, sr непосредственно предшествуют 2|| состояний вида s, s0,…, sr1, где s (). Пусть Q1 Q(r, ). Обозначим N(Q1) множество всех состояний, непосредственно следующих за состояниями из Q1, а P(Q1) -- аналогичное множество для отношения P. Если компоненты вектора si в состоянии q = s0, s1, …, sr рассматривать как истинностные значения соответствующих атомов ранга i r при некотором упорядочении множества , то можно говорить о значении формулы Ft на состоянии q. Формулу F(t) будем рассматривать как способ задания множества Q(F(t)) состояний из Q(r, ), а именно, тех состояний, на которых она истинна. Ограничения отношений N и P на множество Q(F(t)) обозначим соответственно NF и PF.

Пусть G(F) -- граф отношения NF. Граф G = <V, E>, где V -- множество вершин, а E -- множество дуг графа, назовем циклическим, если для каждой его вершины q существуют дуги (q1, q) и (q, q2), принадлежащие E. Спецификация F = tF(t) непротиворечива тогда и только тогда, когда граф G(F) имеет непустой циклический подграф [4]. Множество состояний (вершин) максимального такого подграфа G*(F) графа G(F) назовем ядром множества Q(F(t)).

Понятие состояния можно определить как отрезок длины r + 1 сверхслова, соответствующего интерпретации формулы глубины r. Если формула глубины r истинна на состоянии q, соответствующем отрезку u(, + r) интерпретации u, то она истинна в позиции + r этой интерпретации. Каждая модель u для формулы F = tF(t) однозначно определяет такое двустороннее сверхслово состояний … q-2, q-1, q0, q1, q2, …, что для каждого i Z qi+1 N(qi), и наоборот, каждое такое двустороннее сверхслово состояний, принадлежащих Q(F(t)), однозначно определяет модель для формулы F.

Утверждение 1. Пусть Q* -- ядро множества состояний Q(F(t)), тогда для каждого состояния q из Q* существует модель u для формулы tF(t), содержащая отрезок, совпадающий с состоянием q.

Пусть Q и Q -- такие подмножества множества Q(F(t)), что PF(Q ) = Q и NF(Q ) = Q. Для проверки непустоты графа G*(F) достаточно построить одно из множеств -- Q или Q. Таким образом, эта проверка может быть выполнена одним из следующих алгоритмов. Первый алгоритм состоит в построении последовательности множеств состояний: Q0 = Q(F(t)), Q1 = Q0 N(Q0), …, Qi+1 = Qi N(Qi), … до тех пор, пока для некоторого k не выполнится Qk1 = Qk. Если при этом Qk , то множество вершин графа G*(F) также не пусто, и наоборот, Qk = свидетельствует о его пустоте. Второй алгоритм использует отношение P и аналогичным образом строит последовательность: Q0 = Q(F(t)), Q1 = Q0 P(Q0), …, Qi+1 = Qi P(Qi), … . Условия окончания и результат определяются так же, как и для первого алгоритма. Результаты применения данных алгоритмов к множеству состояний Q обозначим соответственно N*(Q) и P*(Q). Рассмотрим некоторые свойства этих множеств.

Утверждение 2. Справедливо равенство N*(P*(Q)) = P*(N*(Q)) = Q*, где Q* -- ядро множества состояний Q.

Утверждение 3. Каждое состояние множества N*(Q) достижимо из некоторого состояния этого множества, т.е. из q N*(Q) следует P(q) .

Утверждение 4. Из каждого состояния множества P*(Q) достижимо некоторое состояние этого множества, другими словами, из каждого состояния множества P*(Q) достижимо его ядро.

Лемма 1. Пусть Q1 Q, тогда N*(Q1) N*(Q) и P*(Q1) P*(Q).

Справедливость этой леммы вытекает из следующих очевидных равносильностей: N(Q1 Q2) = N(Q1) N(Q2) и P(Q1 Q2) = P(Q1) P(Q2).

Утверждение 5. Пусть Q1 N*(Q), тогда P*(Q1) Q*, где Q* -- ядро множества Q.

Это утверждение следует на основании леммы 1 из P*(N*(Q)) = Q* и Q1 N*(Q).

Обозначим P(F(t)) формулу, задающую множество всех тех состояний из Q(r, ), которые непосредственно предшествуют состояниям из множества Q(F(t)), а N(F(t)) -- формулу, задающую множество всех состояний, непосредственно следующих за состояниями из этого множества. Как показано в [4], для F(t), заданной в д.н.ф., P(F(t)) получается, если в каждой элементарной конъюнкции, входящей в F(t), удалить все литеры нулевого ранга и полученную д.н.ф. сдвинуть на 1 вправо, т.е. увеличить ранги всех атомов на 1. Аналогично, N(F(t)) получается, если в каждой элементарной конъюнкции, входящей в д.н.ф. формулы F(t), удалить все литеры минимального ранга (т.е. ранга -r, если таковые имеются) и полученную д.н.ф. сдвинуть на 1 влево. Пересечению множеств состояний соответствует конъюнкция задающих их формул. Таким образом, алгоритмы проверки непротиворечивости формулы tF(t) состоят в итеративном выполнении операции F(t)&P(F(t)) или F(t)&N(F(t)) до стабилизации формулы. Результаты применения этих алгоритмов к формуле F(t) обозначим соответственно P*(F(t)) и N*(F(t)).

При задании формулы F(t) в виде к.н.ф. первый алгоритм сводится к методу R-резолюции [4], для которого получены различные усовершенствования [6, 7].

СВОЙСТВА СПЕЦИФИКАЦИЙ И СПОСОБЫ ИХ ЗАДАНИЯ

Всякая спецификация реактивного алгоритма характеризует совокупность его свойств, выраженных в виде множества сверхслов в алфавите, определяемом спецификацией. Пусть -- конечный алфавит. Свойством над назовем произвольное подмножество множества . Так, формула F языка L сигнатуры задает свойство, определяемое множеством сверхслов W(F) в алфавите (). Спецификация F, с которой ассоциируется алфавит , обладает свойством S тогда и только тогда, когда W(F) S. Будем говорить, что модель формулы F обладает свойством S, если все ее -суффиксы содержатся в S.

Под верификацией спецификации реактивного алгоритма понимается автоматическая проверка наличия у нее требуемых свойств. Свойства, выразимые в языке L, нет необходимости проверять, поскольку соответствующие им формулы должны быть включены в спецификацию алгоритма и полученный в результате синтеза алгоритм будет заведомо обладать этими свойствами. Поэтому при верификации спецификаций в языке L проверяются свойства, не выразимые в этом языке. Для задания таких свойств широкое распространение получили темпоральные логики. В настоящей работе рассматриваются свойства, задаваемые формулами темпоральной логики с линейным временем (LTL), принадлежащими классу GR(1) [2].

Формулы рассматриваемой темпоральной логики строятся из символов атомарных высказываний, принадлежащих множеству = {p1, p2 , …, pm}, с помощью пропозициональных связок и унарных темпоральных операторов X, G, F. В качестве области интерпретации выступает множество всех сверхслов в алфавите (). Здесь символы алфавита удобно трактовать как подмножества множества . Для определения семантики формулы используется понятие ее истинностного значения в позиции i сверхслова, соответствующего интерпретации (()).

Приведем индуктивное определение истинности формулы в позиции i сверхслова = 123….

Формула p, где p , истинна тогда и только тогда, когда p i.

Формула X истинна тогда и только тогда, когда истинна в позиции i +1 сверхслова .

Формула G истинна тогда и только тогда, когда истинна во всех позициях j i сверхслова .

Формула F истинна тогда и только тогда, когда существует такое j i, что формула истинна в позиции j сверхслова .

Значение истинности формул 1, 12, 1&2 определяется обычным образом.

Формула истинна в интерпретации , если она истинна в позиции 1 соответствующего сверхслова. Таким образом, каждая формула задает множество W() сверхслов в алфавите (), т.е. множество всех тех сверхслов, на которых она истинна.

Формулы из класса GR(1) имеют вид (GF1 & … & GFm) (GF1 & … & GFn), где формулы i (i = 1, …, m) и j (j = 1, …, n) построены из атомарных высказываний с помощью пропозициональных связок и темпорального оператора X.

Для верификации спецификаций в языке L удобно иметь один и тот же язык для представления спецификаций и их свойств. В качестве такого языка будем использовать язык Lmax, формулы которого интерпретируются на множестве Z целых чисел. Это язык логики предикатов первого порядка с одноместными предикатами из множества = {p1, …, pm} и одним двуместным предикатом , интерпретируемым как отношение линейного порядка на Z. Множество термов языка имеет вид T = {(ti + k) | ti V, k Z}, где V = {t, t1, t2, …} -- множество предметных переменных. Имеется два типа атомарных формул: формулы вида p(), где p , а T, и формулы вида (1 2), где 1, 2 T. Так же, как и для языка L, с каждой формулой F языка Lmax ассоциируется множество W(F) сверхслов в алфавите ().

Определим отображение формул языка GR(1) в формулы Lmax:

(p) = p(t), где p ;

(X) = F(t+1),

где F(t) = (), например,

(Xp) = р(t+1), а (XXXp) = р(t+3);

() = (());

если -- произвольная двуместная пропозициональная связка, то

(1 2) = (1) (2);

(GF1) = tt1(t1 t)F1(t1), а (FG1) = tt1((t1 t) F1(t1)), где F1(t) = (1).

Можно показать, что если GR(1), то W() = W(()), т.е. формулы и () определяют одно и то же свойство. Это позволяет при верификации вместо формул языка GR(1) использовать соответствующие формулы языка Lmax, интерпретируемые на множестве целых чисел.

В заключение раздела рассмотрим формулу G(1 F2), где 1 и 2 не содержат операторов G и F. Эта формула не принадлежит классу GR(1), однако выражает важный класс свойств, которые часто необходимо проверять при верификации спецификаций алгоритмов. Формула языка Lmax, задающая это же свойство, имеет вид t(F1(t) t1(t1 t)F2(t1)), где F1(t) = (1), а F2(t) = (2). Далее будет показано, что предлагаемый подход может использоваться для проверки и такого рода свойств.

ПРОВЕРКА СВОЙСТВ БЕЗ УЧЕТА ИНФОРМАЦИИ О СРЕДЕ.

Наиболее простое свойство , выразимое в GR(1) и не выразимое в языке L, имеет вид GF1. В языке Lmax ему соответствует формула tt1(t1 t)F1(t1), где F1(t) не содержит кванторов. Всякое сверхслово, принадлежащее этому свойству, имеет бесконечно много позиций, в которых истинна формула F1(t). Таким образом, спецификация F = tF(t) не обладает этим свойством тогда и только тогда, когда для нее существует такая модель u, что, начиная с некоторой позиции , формула F1(t) истинна на u для всех t . Пусть глубина формулы F(t) равна r, тогда в интерпретации u найдутся такие две позиции i и j ( i j), что u(i -r, i) = u(j-r, j). Двустороннее сверхслово (u(i + 1, j))Z также является моделью для F. Эта модель обладает свойством tF1(t), поэтому из того, что существует модель, не обладающая свойством , следует, что существует модель, обладающая свойством tF1(t). В то же время, если существует модель, обладающая свойством tF1(t), то очевидно, что спецификация F не обладает свойством . Итак, спецификация F не обладает свойством тогда и только тогда, когда формула tF(t)&F1(t) непротиворечива. Поскольку это формула языка L, ее непротиворечивость легко проверяется, например, методом R-резолюции [4].

Как уже отмечалось, важное значение имеет свойство, выражаемое формулой = t(F1(t) t1(t1 t)&F2(t1)), где F1(t) и F2(t1) -- формулы языка L, не содержащие кванторов.

Сначала рассмотрим ситуацию, в которой F1(t) сохраняет истинное значение вплоть до момента t1, когда становится истинной формула F2(t). Более точно эта ситуация выражается формулой t(F1(t)&F2(t)&F2(t + 1) F1(t + 1)). В этом случае свойство может быть заменено свойством = tt1(t1 t)&(F1(t1) F2(t1)), утверждающим, что формула F1(t)&F2(t) не сохраняет истинное значение бесконечно долго. Таким образом, задача сводится к рассмотренной выше проверке свойства вида GF1, т.е. к проверке противоречивости формулы tF(t)&F1(t)&F2(t).

Рассмотрим теперь случай, когда F1(t) не сохраняет истинное значение до момента t1. Спецификация F не обладает свойством тогда и только тогда, когда для нее существует модель с -суффиксом, в начальной позиции которого истинна F1(t), а во всех остальных позициях, включая начальную, ложна F2(t). Определить наличие такой модели можно следующим образом. Как описано ранее, строим формулу N*(F(t)) и умножаем ее на F2(t). Затем для полученной формулы F (t) = N*(F(t))&F2(t) строим формулу P*(F (t)) и умножаем ее на F1(t). Спецификация tF(t) не обладает свойством тогда и только тогда, когда это произведение не равно тождественно 0. Покажем справедливость этого утверждения. Пусть Q -- множество состояний, задаваемое формулой P*(F (t)).

Если конъюнкция P*(F (t))&F1(t) не равна тождественно 0, то Q содержит состояние q, на котором истинна формула F1(t)&F2(t). Из утверждений 1 и 5 следует, что для спецификации F существует модель u, в некоторой позиции которой истинна формула F1(t)&F2(t). Из утверждения 4 следует, что из состояния q достижимо ядро множества Q. Таким образом, для спецификации F существует модель, в позиции которой истинна формула F1(t)&F2(t), а во всех остальных позициях ложна формула F2(t). Это означает, что спецификация F не обладает свойством .

Пусть состояние q, на котором истинна формула F1(t), не принадлежит множеству Q, т.е. P*(F(t))&F1(t) = 0. Тогда либо на этом состоянии истинна формула F2(t), либо из него не достижимо ядро множества Q, т.е. любая модель, содержащая отрезок, соответствующий состоянию q, не имеет -суффикса, в начальной позиции которой истинна формула F1(t)&F2(t), а во всех остальных позициях ложна формула F2(t). Таким образом, если конъюнкция P*(F (t))&F1(t) равна тождественно 0, то спецификация обладает свойством .

Пример. Формула F(t) в спецификации F = tF(t) имеет вид

y(t-2)x(t-1)y(t-1)(x(t)y(t) x(t)y(t)) x(t-1)y(t) y(t-2)y(t-1)x(t)y(t),

а проверяемое свойство задано формулой t(x(t) t1(t1 t)y(t1)). Автомат, специфицируемый формулой F, приведен на рис. 1.

Процесс верификации выглядит следующим образом.

Рис. 1

В соответствии с приведенным алгоритмом строим сначала формулу N*(F(t)):

N(F(t)) = x(t-2)y(t-2)(x(t-1)y(t-1) x(t-1)y(t-1)) x(t-2)y(t-1) y(t-2)x(t-1)y(t-1);

F1(t) = N(F(t)) & F(t) = x(t-2)x(t-1)y(t-1)y(t) y(t-2)x(t-1)y(t-1)(x(t)y(t) x(t)y(t)) x(t-2)y(t-2)x(t-1)y(t) x(t-2)y(t-2)y(t-1)x(t)y(t);

N(F1(t)) = x(t-2)y(t-2)(x(t-1)y(t-1) x(t-1)y(t-1)) x(t-2)y(t-1) y(t-2)x(t-1)y(t-1).

Поскольку N(F1(t)) = N(F(t)), на этом процесс построения N*(F(t)) заканчивается и N*(F(t)) = F1(t). Умножение F1(t) на y(t) дает следующую формулу F (t):

F (t) = F1(t)&y(t) = x(t-2)x(t-1)y(t-1)y(t) y(t-2)x(t-1)y(t-1)x(t)y(t) x(t-2)y(t-2)x(t-1)y(t) x(t-2)y(t-2)y(t-1)x(t)y(t).

Далее строим формулу P*(F (t)):

P(F(t)) = x(t-1)x(t)y(t) y(t-1)x(t)y(t) x(t-1)y(t-1)x(t) x(t-1)y(t-1)y(t).

Несложно убедиться, что формула P(F (t))&F (t) эквивалентна F (t), поэтому процесс построения P*(F (t)) заканчивается и P*(F (t)) = F (t).

Произведение F (t) на x(t) не равно тождественно 0, и, следовательно, верифицируемая спецификация F не обладает свойством . Конец примера.

Верифицируемый алгоритм обладает свойством = 1&2 тогда и только тогда, когда он обладает свойством 1 и обладает свойством 2, поэтому проверка свойства сводится к двум независимым проверкам свойства 1 и свойства 2.

ВЕРИФИКАЦИЯ ОТКРЫТЫХ СИСТЕМ.

При верификации открытых систем [8] достаточно ограничиться рассмотрением двух компонентов такой системы: собственно алгоритма и его среды. При этом чаще всего в качестве верифицируемого алгоритма выступает спецификация его управляющей части, а в качестве среды -- объединенная спецификация операционной части и внешней среды. Проверяемые свойства, как правило, имеют вид e s, где e -- свойство среды, а s -- свойство верифицируемого алгоритма. Формулам e и s в языке GR(1) соответствуют конечные конъюнкции формул языка L и формул вида tt1(t1 t)F1(t1).

Рассмотрим сначала случай, когда формулы e и s имеют соответственно вид tt1(t1 t)F1(t1) и tt1(t1 t)F2(t1). Спецификация не обладает свойством e s тогда и только тогда, когда она имеет хотя бы одну модель, не обладающую этим свойством, т.е. обладающую свойством es. Вообще говоря, утверждения «модель не обладает свойством » и «модель обладает свойством » не равносильны. Свойство S называется суффиксно замкнутым, если из того, что сверхслово принадлежит S, следует, что любой его -суффикс также принадлежит S. Учитывая, что свойства, выразимые формулами GF и FG, суффиксно замкнуты, несложно показать, что свойства, выразимые формулами языка GR(1), и их дополнения суффиксно замкнуты. Для таких свойств модель не обладает свойством тогда и только тогда, когда она обладает свойством . Таким образом, спецификация не обладает свойством e s тогда и только тогда, когда для нее существует модель с -суффиксом, обладающим следующими свойствами: а) во всех его позициях истинна формула F2(t); б) имеется бесконечное количество позиций, в которых истинна формула F1(t). Проверка существования такой модели осуществляется следующим образом. Пусть Q -- множество состояний, задаваемое формулой F(t)&F2(t). Выделим в Q все состояния, на которых истинна F1(t), что на уровне формул соответствует формуле F(t)&F2(t)&F1(t). Если эта формула тождественно равна нулю, то процесс верификации заканчивается с положительным результатом. В противном случае необходимо определить, содержит ли множество состояний Q1, задаваемое рассматриваемой формулой, состояние, достижимое из себя. Если Q1 содержит такое состояние, то оно принадлежит ядру множества Q, а это означает, что для верифицируемой спецификации существует модель, являющаяся моделью для формулы tF2(t) и имеющая -суффикс с бесконечным количеством позиций, в которых истинна формула F1(t). Если такой модели не существует, то никакая модель не обладает свойством es и, следовательно, спецификация обладает проверяемым свойством. Для проверки наличия в множестве Q1 такого состояния строим множество всех тех состояний из Q, которые достижимы (в смысле отношения N) из Q1, и берем пересечение этого множества с Q1. Возможны три ситуации: верификация реактивный алгоритм спецификация

1) если пересечение пусто, то Q1 не содержит состояния, достижимого из себя;

2) если пересечение совпадает с Q1, то Q1 содержит такое состояние;

3) если пересечение не пусто и равно Q2 Q1, где Q2 не совпадает с Q1, то переходим к проверке наличия в Q2 состояния, достижимого из себя, и т.д.

Проверка свойства завершается при возникновении первой или второй ситуации.

Осталось уточнить процедуру построения множества всех тех состояний из Q, которые достижимы из заданного множества Q1 Q. Обозначим это множество N +(Q1). В основе процедуры лежит итеративное применение операции N(Qi). Сначала получаем множество Q2 = N(Q1) Q, затем для i = 2, 3, … строим последовательность Qi+1 = (N(Qi) Q) Qi ,пока не получим Qi+1 = Qi = N +(Q1). На уровне формул последняя операция имеет вид Fi+1(t) = N(Fi(t))&F(t) Fi(t).

Возможны модификации этого алгоритма, например, его можно начинать с проверки свойства s, т.е. с проверки противоречивости формулы tF(t)&F2(t). Если спецификация обладает этим свойством, то проверка заканчивается. Если проверяемая формула непротиворечива, формула, полученная в результате проверки, умножается на F1(t) и дальше процесс протекает так, как описано ранее.

Рассмотрим свойство 1 2&3. Поскольку (1 2&3) (1 2)&(1 3), его проверка сводится к проверке двух свойств рассмотренного ранее вида.

Пусть теперь проверяемое свойство имеет вид 1&2 3, где i = tt1(t1 t)Fi(t1) (i = 1, 2, 3). Спецификация обладает этим свойством тогда и только тогда, когда все модели, имеющие -суффикс, во всех позициях которого истинна формула F3(t), имеют либо -суффикс, во всех позициях которого истинна F1(t), либо -суффикс, во всех позициях которого истинна F2(t). Таким образом, спецификация не обладает свойством 1&2 3 тогда и только тогда, когда в множестве состояний, задаваемых формулой F(t)&F3(t), имеются два состояния -- q1 и q2, на которых истинны соответственно формулы F1(t) и F2(t) и такие, что q2 достижимо из q1, а q1 достижимо из q2. Пусть Q -- множество состояний, задаваемое формулой F(t)&F3(t), а Q10 и Q20 -- множества всех тех состояний из Q, на которых истинны соответственно F1(t) и F2(t). Строим множество всех тех состояний из Q, которые достижимы из Q10 (N +(Q10)), и берем его пересечения с Q10 и Q20. В результате получим множества Q11 Q10 и Q21 Q20. Затем строим множество N +(Q21) и берем его пересечения с Q11 и Q21, что дает множества Q12 Q10 и Q22 Q20, и т.д. В итоге будут получены две последовательности: Q10 Q11 Q12 … и Q20 Q21 Q22 … . Процесс заканчивается, когда хотя бы одно из множеств этих последовательностей будет пусто, либо в каждой последовательности два смежных множества будут равны. В первом случае спецификация обладает свойством 1&2 3, во втором -- не обладает. Очевидно, что приведенный алгоритм легко распространяется на проверку свойства, задаваемого импликацией с k 2 сомножителями в левой части. Обозначим их 0, 1, …, k-1, а множества состояний из Q, на которых истинны соответственно формулы F0(t), F1(t), …, Fk-1(t), -- как Q00, Q10, …, Q(k-1)0. Процесс дальнейшего вычисления состоит в построении для j = 0, 1, …, k - 1 последовательностей Qj0 Qj1 Qj2 … . На i-й итерации вычисляются очередные k членов этих последовательностей в соответствии с формулой Qj(i+1) = N +(Q(i mod k)i) Qji (j = 0, 1, …, k - 1). Условия окончания процесса те же, что и выше.

Вычисление всех состояний, достижимых из заданного множества состояний, представляет собой незначительную модификацию проверки непротиворечивости, основанной на итеративном вычислении N(F(t)) для формулы F(t) языка L. Таким образом, легко видеть, что проверка свойства, заданного формулой языка GR(1), сводится к проверкам непротиворечивости формул языка L.

Рассмотрены методы верификации спецификаций реактивных алгоритмов относительно свойств, выразимых формулами из класса GR(1) темпоральной логики LTL. Следует подчеркнуть, что речь идет о верификации декларативных спецификаций, представленных в виде формул логического языка, а не императивных представлений алгоритмов в терминах состояний и отношений переходов. Процесс верификации сводится к преобразованию формул языка L, рассматриваемых как пропозициональные формулы, в качестве переменных которых выступают атомы языка L. Для этой цели используются средства для проверки непротиворечивости спецификаций в языке L и некоторые другие средства проектирования алгоритмов, рассматриваемых как открытые системы.

Хотя в статье речь идет о формулах из класса GR(1), нетрудно заметить, что на самом деле рассматривается более широкий класс темпоральных формул. Так, в подформулах i формул вида GFi допускается использование оператора X, а в качестве множителей, составляющих формулу s, могут выступать также формулы вида G(1 F2). Возможны и другие расширения класса GR(1), однако все они ограничены формулами, задающими суффиксно замкнутые свойства, поскольку только для таких формул существуют формулы языка Lmax, задающие те же свойства.

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

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

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

1. Чеботарев А.Н. Об одном подходе к функциональной спецификации автоматных систем // Кибернетика и системный анализ. -- 1993. -- № 3. -- С. 31-42.

2. Piterman N., Pnueli A., Sa'ar Y. Synthesis of reactive(1) designs // Proc. Conf. on Verification, Model Checking and Abstract Interpretation. -- 2006. -- P. 364-380.

3. Lichtenstein O., Pnueli A. Checking that finite state concurrent programs satisfy their linear specification // Proc. 12th Symp. on Principles of Programming Languages (New York, ACM). -- 1985. -- P. 97-107.

4. Чеботарев А.Н. Проверка непротиворечивости простых спецификаций автоматных систем // Кибернетика и системный анализ. -- 1994. -- № 3. -- С. 3-11.

5. Крывый С.Л., Чеботарев А.Н. Проверка непротиворечивости формул языка L, представленных в дизъюнктивной нормальной форме. I // Там же. -- 2005. -- № 4. -- С. 22-28.

6. Чеботарев А.Н. Метод раздельного резольвирования для проверки выполнимости формул языка L // Там же. -- 1998. -- № 6. -- С. 13-20.

7. Кривой С.Л., Чеботарев А.Н. Усовершенствованный метод проверки выполнимости множества дизъюнктов в языке L // Таврич. вестн. информатики и математики. -- 2006. -- № 1, -- С. 7-13.

8. Pnueli A., Rosner R. On the synthesis of a reactive module // Proc. 16th Ann. Symp. on Principles of Programming Languages (New York, ACM). -- 1989. -- P. 179-190.

Размещено на Allbest.ru