Software & Systems

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

Концептуальная особенность данного метода в том, что верификация выполняется путем анализа свойств моделей систем, построенных на базе некоторых формальных конструкций, относительно требований к ним, также заданных формально. Как правило, для задания требований оперируют такими временными логиками, как LTL, CTL, CTL* [3–6]. Однако выразительные способности этих логик не являются безграничными и в некоторых случаях невозможно задать с их помощью необходимые требования.

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

Логика CTL [6] является альтернативным по отношению к LTL способом формулирования временных свойств. Если в логике линейного времени свойства формулируются лишь относительно некоторого порядка их наступления внутри вычислительного процесса, то в логике ветвящегося времени, помимо порядка, учитываются также сами альтернативы развития вычислительного процесса. В отличие от логики линейного времени, формулы которой являются формулами пути, формулы логики ветвящегося времени являются формулами состояний. То есть любой темпоральный оператор формулы CTL предварен квантором пути, который определяет, на всех (квантор всеобщности A) или только на некоторых (квантор существования E) путях из текущего состояния соответствующая формула является истинной [1].

Верифицируемая система может работать в разных режимах в зависимости от условий или исходных данных, может поддерживать многопоточное/многопроцессное выполнение [9] или результаты работы системы носят вероятностный характер [10]. Во всех этих ситуациях логики линейного времени, скорее всего, будет недостаточно.

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

RTL-нотация

Предложенная авторами в работе [6] RLTL-нотация позволяет представлять операторы LTL и их композиции в виде систем рекурсивных уравнений (см. табл. 1, 2).

Таблица 1

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

Table 1

Recursive representations of LTL operators in RLTL

Таблица 2

Примеры представления композиций операторов LTL в RLTL

Table 2

The examples of composition representations of LTL operators in RLTL

Формулам LTL в RLTL-нотации соответствуют системы рекурсивных уравнений. В левой части каждого уравнения записывается метапеременная, уникально идентифицирующая данное уравнение, в правой – темпоральное выражение, содержащее как метапеременные, так и терминальные символы (предикаты).

Замечание. Не следует путать использование метапеременных F, G и U в рекурсивных уравнениях с одноименными темпоральными операторами.

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

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

Унифицированная нотация логик LTL и CTL, далее именуемая RTL-нотацией, представляет собой RLTL-нотацию, расширенную и дополненную рядом аксиом и условных обозначений формул логики ветвящегося времени. Для расширения RLTL-нотации в RTL следует ввести следующие допущения:

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

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

В таблице 3 представлены все основные операторы логики CTL и соответствующие им синтаксические конструкции RTL.

Таблица 3

Рекурсивные представления операторов CTL в RTL-нотации

Table 3

Recursive representations of CTL operators in RTL notation

Обозначим через 𝒫(C) множество всех последовательностей предикатов, соответствующих формуле C логики ветвящегося времени, а через 𝒫(R(C)) – множество всех последовательностей предикатов, соответствующих представлению формулы C в RTL.

Теорема 1. Для всех формул C логики ветвящегося времени 𝒫(C) = 𝒫(R(C)).

Доказательство. Формула AXφ означает, что, каким бы ни было значение предиката на данном шаге, на следующем шаге будет истинным значение преди- ката φ. Запись ∆ ∘ φ означает, что на данном шаге вы- полняется некоторое неопределенное множество пре- дикатов (возможно, пустое), а на следующем шаге будет истинным значение предиката φ, что в точности совпадает со смыслом формулы AXφ.

Рассмотрим также доказательство теоремы для формулы EGφ. В соответствии с семантикой этой формулы в CTL множество последовательностей включает в себя, по крайней мере, одну ветвь, для которой на данном шаге справедливо утверждение (предикат) φ, а на каждом следующем шаге, опять же хотя бы в одной ветви, являющейся продолжением данной ветви, справедливо утверждение φ. Из представления данной формулы в RTL нетрудно понять, что на данном шаге хотя бы в одной ветви должно быть справедливым утверждение φ, а на каждом следующем шаге, опять же хотя бы в одной ветви, являющейся продолжением данной ветви, справедливо утверждение φ, что в точности совпадает со смыслом формулы EGφ.

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

Если сделать предположение о том, что бесконечно повторяющаяся альтернатива должна быть когда-нибудь выбрана, то нетрудно осуществить и обратный переход от представлений формул в RTL к исходным формулам CTL.

Отметим, что RTL представляет собой именно нотацию для представления формул логик LTL и CTL, поскольку базируется на их семантических определениях, но никак не отдельную логику.

Сформулируем аксиомы и правила вывода нотации RTL, задающие систему эквивалентных преобразований формул CTL. Cимволом γ (с индексами и без) будем обозначать темпоральные выражения.

Аксиомы RTL:

A1. ˥Fγ = G˥γ

A2. ˥Gγ = F˥γ

A3. ˥Aγ = E˥γ

A4. ˥Eγ = A˥γ

A5. ˥∆ = ∆

A6. ∆⍵ ∘ γ = ∆⍵

A7. ∆⍵ = ∆ ∘ ∆⍵

A8. γ1 + γ2 = γ2 + γ1

A9. γ + γ = γ

A10. (γ1 + γ2) + γ3 = γ1 + (γ2 + γ3)

A11. γ1 ∘ (γ2 ∘ γ3) = (γ1 ∘ γ2) ∘ γ3

A12. (γ1 + γ2) ∘ γ3 = γ1 ∘ γ3 + γ2 ∘ γ3

A13. γ1 ∘ (γ2 + γ3) = γ1 ∘ γ2 + γ1 ∘ γ3

Правила вывода RTL:

R1. F = γ1 ∘ F ∘ γ2 → F = γ1 ∘ F

R2. F = γ1 ∘ F → F = γ1 ∘ F ∘ γ2 (и в обратную сторону правило справедливо)

Сочетания операторов CTL

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

Утверждение 1. Выражение вида AGAFφ логики CTL может быть представлено в RTL-нотации в виде F = φ ∘ F + ∆ ∘ F.

Доказательство. Обозначим через F выражение AGAFφ = AG(AFφ), а через F1 выражение AFφ.

F = AGAFφ = AG(AFφ) = (п. 5 табл. 3)

F1 ∘ F = (п. 3 табл. 3)

(φ + ∆ ∘ F1) ∘ F = (A12)

φ ∘ F + ∆ ∘ F1 ∘ F = (A11)

φ ∘ F + ∆ ∘ (F1 ∘ F) =

φ ∘ F + ∆ ∘ F, ч.т.д.

Утверждение 2. Выражение вида AGEFφ логики CTL может быть представлено в RTL-нотации в виде F = φ ∘ F + ∆ ∘ (F + ∆⍵).

Доказательство. Обозначим через F выражение AGEFφ = AG(EFφ), а через F1 выражение EFφ.

F = AGEFφ = AG(EFφ) = (п. 5 табл. 3)

F1 ∘ F = (п. 4 табл. 3)

(φ + ∆ ∘ (F1 + ∆⍵)) ∘ F = (A12)

φ ∘ F + ∆ ∘ (F1 ∘ F + ∆⍵ ∘ F) = (A6)

φ ∘ F + ∆ ∘ (F + ∆⍵), ч.т.д.

Утверждение 3. Выражение вида AFAGφ логики CTL может быть представлено в RTL-нотации в виде системы рекурсивных уравнений:

F = φ ∘ F1 + ∆ ∘ F

F1= φ ∘ F1

Доказательство. Обозначим через F выражение AFAGφ = AF(AGφ), а через F1 выражение AGφ.

F = AFAGφ = AF(AGφ) = (п. 3 табл. 3)

F1 + ∆ ∘ F = (п. 5 табл. 3)

φ ∘ F1+ ∆ ∘ F

F1 = φ ∘ F1 (п. 5 табл. 3), ч.т.д.

Утверждение 4. Выражение вида AFEGφ логики CTL может быть представлено в RTL-нотации в виде системы рекурсивных уравнений:

F = φ ∘ (F1+ ∆⍵) + ∆ ∘ F

F1 = φ ∘ (F1 + ∆⍵)

Доказательство. Обозначим через F выражение AFEGφ = AF(EGφ), а через F1 выражение AEφ.

F = AFEGφ = AF(EGφ) = (п. 3 табл. 3)

F1 + ∆ ∘ F = (п. 6 табл. 3)

φ ∘ (F1 + ∆⍵) + ∆ ∘ F

F1 = φ ∘ (F1 + ∆⍵) (п. 6 табл. 3), ч.т.д.

Докажем также теорему, существенно упрощающую формулировку некоторых верифицируемых условий.

Теорема 2. Справедливы следующие равенства:

1.    AFAFφ = AFφ;

2.    EFEFφ = EFφ;

3.    AGAGφ = AGφ;

4.    EGEGφ = EGφ.

Доказательство п. 1. Обозначим через F1 выражение AFAFφ, а через F2 выражение AFφ.

F1 = AFAFφ = F2 + ∆ ∘ F1 = φ + ∆ ∘ F2 + ∆ ∘ F1 =

= (A13) = φ + ∆ ∘ (F2 + F1) = φ + ∆ ∘ F3

F3 = (F2 + F1) = φ + ∆ ∘ F2 + ∆ ∘ (F2 + F1) = =(A13) =

= φ + ∆ ∘ (F2 + F2 + F1) = φ + ∆ ∘ (F2 + F1) = φ + ∆ ∘ F3.

Таким образом, для левой части равенства получаем систему из двух рекурсивных уравнений:

F1 = φ + ∆ ∘ F3

F3 = φ + ∆ ∘ F3.

Очевидно, что рекурсивное уравнение, представляющее выражение AFφ, можно расширить до системы уравнений вида

F1¢ = φ + ∆ ∘ F2¢

F2¢ = φ + ∆ ∘ F2¢.

Получаем систему уравнений, совпадающую с си- стемой уравнений для левой части равенства 1 с точ- ностью до переименования метапеременных, а следовательно, задающую то же самое множество последовательностей, ч.т.д.

Аналогичным образом нетрудно доказать справедливость равенств 2–4.

Примеры

Рассмотрим три примера для лучшего понимания принципов задания формул ветвящегося времени на базе RTL.

1. F = ∆ ∘ (Gφ1 + Gφ2). Формула истинна, если «из текущего состояния исходят два типа ветвей: либо во всех состояниях выполняется φ1, либо во всех состояниях выполняется φ2».

2. F = φ1 ∘ (Gφ3 + Gφ4) + φ2 ∘ Gφ5. Формула истинна, если «в текущем состоянии выполняется φ1 или φ2, при этом, если выполняется φ1, то из текущего состояния исходят два типа ветвей: либо во всех состояниях выполняется φ3, либо во всех состояниях выполняется φ4; если в текущем состоянии выполняется φ2, то исходят лишь те ветви вычислительных последовательностей, для которых во всех состояниях истинно φ5».

3. F = φ ∘ (F + ∆⍵). Формула истинна, если «в текущем состоянии выполняется φ и из него исходит хотя бы одна ветвь, в которой будет истинна эта же формула».

На рисунке представлены развертки моделей, удовлетворяющие примерам 1–3 соответственно.

Отметим, что переход в некоторое состояние, помеченное каким-либо символом предиката (например, предикатом φ), отображает на самом деле все множество переходов в состояния, в которых выполняется этот предикат.

Заключение

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

задачи Model Checking и ее сложности с помощью RTL-нотации будут подробно рассмотрены в последующих работах.

Таким образом, RTL-нотация в целом представляет собой гибкий и мощный механизм, расширяющий выразительность обеих логик (LTL и CTL) и делающий процесс верификации более эффективным и удобным. В силу своих особенностей RTL может стать единым универсальным инструментом для выполнения всесторонних проверок свойств моделей, позволив специалистам по верификации избавиться от необходимости выполнять лишние действия, связанные с использованием большого числа различных структур данных и подходов к верификации.

Литература

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

2.     Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. М.: МЦНМО, 2002. 416 с.

3.     Pnueli A. The temporal logic of program. Proc. 18th Anny. Symp. on Foundation of Computer Science, 1977, pp. 46–57.

4.     Manna Z., Pnueli A. The temporal logic of reactive and concurrent systems. Specification, 1992, 427 p.

5.     Kroger F., Merz S. Temporal logic and state systems. Springer, 2008, 436 p.

6.     Huth M., Ryan M. Logic in computer science: modelling and reasoning about systems. Cambridge Univ. Press, 2004, 443 p.

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

8.     Кораблин Ю.П., Шипов А.А. Построение моделей систем на базе эквациональной характеристики формул LTL // Програм- мные продукты и системы. 2017. № 1. С. 61–66.

9.     Olderog E.-R., Apt K.R. Fairness in parallel programs: the transformational approach. ACM Transactions on Programming Languages and Systems, 1988, vol. 10, no. 3, pp. 420–455.

10.  Yongming Li, Yali Li, Zhanyou Ma. Computation tree logic model checking based on possibility measures. Fuzzy Sets and Systems, 2015, vol. 262, pp. 44–59.

References

1. Karpov Yu.G. Model Checking. Verification of Parallel and Distributed Software Systems. St. Petersburg, BHV-Peterburg Publ., 2010, 552 p.
2. Clarke E.M., Grumberg O., Peled D.A. Model Checking. MIT Press, Cambridge, MA, USA, 1999 (Russ. ed.: Moscow, MTsNMO Publ., 2002, 416 p.).
3. Pnueli A. The temporal logic of program. Proc. 18th Annyv. Symp. on Foundation of Computer Science. 1977, pp. 46–57.
4. Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. Specification, 1992, 427 p.
5. Kroger F., Merz S. Temporal Logic and State Systems. Springer Publ., 2008, 436 p.
6. Huth M., Ryan M. Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge Univ. Press, 2004,
   443 p.
7. Korablin Yu.P., Shipov A.A. LTL formula equational characteristics. Software & Systems. 2015, no. 4, pp. 175–179 (in Russ.).
8. Korablin Yu.P., Shipov A.A. System models construction based on LTL formula equational characteristics. Software & Systems. 2017, no. 1, pp. 61–66 (in Russ.).
9. Olderog E.-R., Apt K.R. Fairness in parallel programs: The transformational approach. ACM Trans. on Programming Languages and Systems. 1988, vol. 10, no. 3, pp. 420–455.
10. Li Y., Li Y., Ma Zh. Computation tree logic model checking based on possibility measures. Fuzzy Sets and Systems. 2015,
    vol. 262, no. 1, pp. 44–59.