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

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

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

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

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

НЕ нашли? Не то? Что вы ищете?

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

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

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

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

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

Значение истинности формул Øj1, j1Új2, j1&j2 определяется обычным образом.

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

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

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

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

x(p) = p(t), где pÎ W;

x(Xj) = F(t+1), где F(t) = x(j), например, x(Xp) = р(t+1), а x(XXXp) = р(t+3);

x(Øj) = Ø(x(j));

если * — произвольная двуместная пропозициональная связка, то x(j1 * j2) = x(j1) * x(j2);

x(GFj1) = "t$t1(t1 ³ t)&F1(t1), а x(FGj1) = $t"t1((t1 ³ t) ® F1(t1)), где F1(t) = x(j1).

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

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

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

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

Как уже отмечалось, важное значение имеет свойство, выражаемое формулой j = "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)). В этом случае свойство j может быть заменено свойством j¢ = "t$t1(t1 ³ t)&(ØF1(t1) Ú F2(t1)), утверждающим, что формула F1(t)&ØF2(t) не сохраняет истинное значение бесконечно долго. Таким образом, задача сводится к рассмотренной выше проверке свойства вида GFj1, т. е. к проверке противоречивости формулы "tF(t)&F1(t)&ØF2(t).

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

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

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

Пример. Формула 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),
а проверяемое свойство j задано формулой "t(x(t) ® $t1(t1 ³ t)y(t1)). Автомат, специфицируемый формулой F, приведен на рис. 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);

Из за большого объема этот материал размещен на нескольких страницах:
1 2 3