Эквациональная характеристика формул LTL

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

№ 4 (112), 2015

УДК 519.767.2 Дата подачи статьи: 22.07.15

DOI: 10.15827/0236-235X. 112.175-179

ЭКВАЦИОНАЛЬНАЯ ХАРАКТЕРИСТИКА ФОРМУЛ LTL

Ю.П. Кораблин, д.т.н., профессор, y.p.k@mail.ru; А.А. Шипов, аспирант, a-j-a-1@yandex.ru

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

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

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

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

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

Ключевые слова: верификация, модель Крипке, автомат Бюхи, формула временной логики, LTL, CTL.

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

Рассмотрим, например, модель работы светофора, представленную на рисунке 1 структурой Крипке [6].

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

И здесь встает проблема, решение которой невозможно в рамках любой из имеющихся логик: определить свойство строгого чередования трех предикатов на бесконечном интервале в случае необходимости его проверки и сформулировать чередование любого произвольного конечного числа предикатов. В общем виде в LTL свойство чередования для предложенного светофора можно определить с помощью оператора X (на следующем шаге) как ф = Xg Л XXr Л XXXy Л XXXXg Л... Несмотря на то, что запись G(g Л Xr Л XXy) кажется интуитивно правильной для данного примера, можно показать, что в действительности она описывает последовательность совершенно иного ха-

Рис. 2. Развертка режима чередования сигналов Fig. 2. A developed view of signal-interleave mode

175

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

№ 4 (112), 2015

рактера. А именно, используя правило G(p Л q) = = G(p) Л G(q), можно представить данную запись в виде G(g) Л G(Xr) Л G(XXy). Применяя правило рекурсивного определения оператора G вида Gp = = p Л X(p) Л XX(p) Л XXX(p)... для каждого из конъюнктов, получим Gg = g Л X(g) Л XX(g) Л XXX(g)...

G(Xr) = Xr Л X(Xr) Л XX(Xr) Л XXX(Xr)...

G(XXy) = XXy Л X(XXy) Л XX(XXy) Л XXX(XXy).

Объединив их, получим последовательность вида ф = g Л X(g Л r) Л XX(g Л r Л y) л XXX(g Л r Л у).

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

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

Эквациональная характеристика операторов LTL

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

Таблица 1

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

Table 1

LTL operators’ recursive presentations

LTL RLTL

Fф = ф V XFф Fф = ф V А о Fф

Оф = ф Л XGф О -6 II -6 О О -6

ф1иф2 = ф2 V ф1 Л X^1^2) и

ф1 Л Xф2 ф1 о ф2

Xф А о ф

Символ «°» обозначает оператор продолжения (конкатенация выражений), что позволяет использовать оператор X в неявном виде, а также упростить его восприятие, в частности, запись ф1 о ф2 будет пониматься как «ф2 следует за ф1». Под символом «А», далее именуемым предикатом неопределенности, будем понимать неопределенное множество предикатов для конкретного состояния вычислительной последовательности относительно тех предикатов, которые принимают в нем истинностные значения.

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

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

Таблица 2

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

Table 2

Equational combinations of LTL operators

LTL RLTL

ЕОф F' = ф о G' V А о F' G' = ф о G'

ОЕф G' = ф о G' V А о F' F' = ф о G' V А о F'

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

RLTL:

A1. 9- II 9-

A2. ООф = Оф

А3. 1Еф = О1ф

A4. Юф = Е1ф

A5. § II -9 о О -9

A6. Еф = ф V А о Еф

A7. Оф V Юф = А

A8. Еф V 1Еф = А

A9. Оф1 о ф2 = Оф1

A10. Еф1 о ф2 = Е

A11. и

А12. 1

А13. 1А = А

А14. А Л ф = ф

А15. < О 9- II 9-

Примеры описания свойств в RLTL-нотации

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

Общий вид данного типа задается системой рекурсивных уравнений Ф:

Fr1 = pi о Fr2,

Fr2 = p2 о Fr3,

Fr(n) = pn о Fri.

176

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

№ 4 (112), 2015

Пример данного типа уже был рассмотрен при описании модели работы светофора. Сформулируем заданное для нее в общем виде условие ф = Xg Л XXr Л XXXy Л XXXXg Л... с помощью эквацио-нальной характеристики:

Frl = 0 о Fr2;

Fr2 = g о Fr3;

Fr3 = r о Fr4;

Fr4 = y о Fr2.

Под символом «0» в дальнейшем будем понимать пустое множество предикатов, означающее, что ни один из предикатов множества AP [6] не принимает значение «истина». Таким образом, сформулированное условие представляет собой систему из четырех рекурсивных уравнений, строго задающих необходимую последовательность предикатов (сигналов светофора).

Еще одним типом свойств, которые нельзя выразить стандартными формулами LTL, является вхождение (появление) вложенных последовательностей предикатов на бесконечной вычислительной последовательности состояний. В общем виде данный тип изображен на рисунке 4.

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

Представим данный тип в виде системы рекурсивных уравнений Ф:

Frl = 0 о Frl V а о Fr2;

Fr2 = а о Fr2 V (а Л b) о Fr3;

Fr(k) = (а Л b) о Fr(k) V а о Fr(k+i);

Fr(k+i) = а о Fr(k+i) V 0 о Fri.

Выключение питания Включение питания ^трансмиттера /

Конец сеанса радиосвязи

Сеанс

"радиосвязи

Неактивный Режим

режим питания

p, t

> Прием/переда-ча сигнала

M

P

Рис. 5. Модель работы трансмиттера спутника Fig. 5. A satellite transmitter operating model

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

Fr1 = 0 о Fr1 V p о Fr2;

Fr2 = p о Fr2 V (p Л t) о Fr3;

Fr3 = (p Л t) о Fr3 V p о Fr4;

Fr4 = p о Fr4 V 0 о Fr1.

Верификация RLTL

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

Ф = Fr1 = 0 о Fr2;

Fr2 = g о Fr3;

Fr3 = r о Fr4;

Fr4 = y о Fr2.

Для выполнения верификации формул RLTL будет использована та же самая методика верификации, что и для формул LTL, описанная в [6].

На первом этапе сформулируем отрицание проверяемого условия, используя аксиомы, приведенные выше:

1Ф = lFr! = 10 V А о lFr2;

lFr2 = lg V А о 1Fr3;

1Fr3 = lr V А о 1Fr5;

1Fr4 = ly V А о 1Fr2.

На втором этапе для полученной системы рекурсивных уравнений построим контрольный автомат. Для упрощения процесса построения контрольного автомата применим аксиому A15 к полу-

В качестве примера можно рассмотреть модель работы подсистемы космического спутника, отвечающую за работу передатчика и приемника радиосигнала (рис. 5).

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

Система рекурсивных уравнений, характеризующая данную

177

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

№ 4 (112), 2015

Рис. 7. Контрольный автомат Бюхи В)Ф

Fig. 7. CheckBuchi automata В)Ф

s

Рис. 8. Автомат Бюхи Bm для модели светофора Fig. 8. Buchi automata Bm for a traffic light model

ченной системе рекурсивных уравнений и получим следующую систему рекурсивных уравнений:

1Ф = Fri = 10 о Fr5 V А о Fr2;

Fr2 = 1g о Fr5 V А о Fr3;

Fr3 = 1r о Fr5 V А о Fr5;

Fr4 = 1y о Fr5 V А о Fr2;

Fr5 = А о Fr5.

На третьем этапе необходимо представить 1Ф в виде автомата Бюхи В1Ф.

Для этого построим такой автомат, в котором состояниям будут сопоставлены переменные Fi нашей рекурсивной системы уравнений, а переходам - предикаты. Как видно из рисунка 7, сделать это достаточно просто. Допускающими состояниями являются те, в которые существует хотя бы один переход по предикату, отличному от предиката неопределенности А.

Теперь построим композицию автомата В1Ф и автомата Bm нашей модели светофора (рис. 8) согласно методу, описанному в [6]. Результатом композиции перехода, помеченного предикатом неопределенности А, с переходом, помеченным некоторым предикатом ф, является переход, помеченный ф, так как неопределенность устраняется. Результат композиции представлен на рисунке 9.

Жирными стрелками показаны переходы, которые достижимы из начального состояния (s1, 1). Очевидно, что из

начального состояния невозможно попасть ни в одно из допускающих состояний, что означает невыполнимость 1Ф, а следовательно, выполнимость Ф. Таким образом, свойство «со второго состояния светофора начинается строгое чередование зеленого, красного и желтого сигналов» действительно выполняется.

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

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

178

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

№ 4 (112), 2015

щие технологии верификации на базе метода Model Checking или проверки на моделях.

Литература

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

2. Hopcroft J.E., Motwani R., Ullman J.D. Introduction to Automata Theory, Languages, and Computation, 3/E - Pearson/Addi-son Wesley, 2007, 535 p.

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

4. Kroger F., Merz S. Temporal Logic and State Systems. Springer (March 27, 2008), 436 p.

5. Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification. 1992, 427 p.

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

7. Кораблин Ю.П., Куликова Н.Л. Логические методы доказательства и тестирования программ // Информационные средства и технологии: тез. докл. Междунар. конф. М.: Изд-во МФИ, 1996. 9 с.

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

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

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

11. Hoare C.A.R. An axiomatic basis for computer programming. Northern Irelan: Queen's Univ. of Belfast, 1969, pp. 576-580.

12. Abraham E., Havelund K. (Eds). Tools and Algorithms for the Construction and Analysis of Systems. Springer (March 24, 2014), 652 p.

13. Berard 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.

DOI: 10.15827/0236-235X.112.175-179 Received 22.07.15

EQUATIONAL CHARACTERISTICS OF LTL FORMULAS Korablin Yu.P., Dr.Sc. (Engineering), Professor, y.p.k@mail.ru;

Shipov A.A., Postgraduate Student, a-j-a-1@yandex.ru

Abstract. Day by day software systems are becoming more and more complex. Therefore, we need to have some useful instruments to check their capability according to specifications, especially large distributed software systems.

Nowadays, to describe the verifying model conditions it is common to use such mechanisms as linear temporal logic (LTL) and computational tree logic (CTL). However, experience has proven that these mechanisms can help formulate only a relatively small set of the same-type conditions. It can complicate the verification process or make it ineffective for a particular system model.

Correct formulation of model's verifying properties is the key problem, as the whole verification process depends on it. Thus, to achieve best results it is required to use powerful tools and techniques, which clearly formulate a wide class of verifying properties.

The article describes a mechanism that can significantly extend the group of formulated conditions according to verifiable models. This effect can be achieved by expanding LTL expressivity using the proposed method, which increases the efficiency of the verification process.

The article provides a set of illustrative examples of the method, which demonstrates its practical application. The article also provides the example of properties verification for a particular model based on the proposed method.

Keywords: verification, Kripke structure, Buchi automaton, temporal logic formula, LTL, CTL.

References

1. Korablin Yu.P. Semantikayazykov raspredelennogoprogrammirovaniya [Distributed Programming Language Semantics]. Study guide. V.P. Kutepov (Ed.). Moscow, MEI Publ., 1996, 102 p.

2. Hopcroft J.E., Motwani R., Ullman J.D. Introduction to Automata Theory, Languages, and Computation. 3/E. Pear-son/Addison Wesley Publ., 2007, 535 p.

3. Velder S.A., Lukin M.A., Shaluto A.A., Yaminov B.R. Verifikatsiya avtomatnykhprogramm [Verification of automata-based programs]. St. -Petersburg, Nauka Publ., 2011, 244 p.

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

5. Manna Z., Pnueli A. The Temporal Logic ofReactive and Concurrent Systems: Specification. 1992, 427 p.

6. Karpov Yu.G. Model Checking. Verifikatsiyaparallelnykh i raspredelennykhprogrammnykh sistem [Model Checking. Verification of parallel and distributed program systems]. BHV-Peterburg Publ., 2010, 552 p.

7. Korablin Yu.P., Kulikova N.L. Logical Proof Methods and Testing Programs. Tezisy, doklad. Mezhdunar. konf. "In-formatsionnye sredstva i tekhnologii ” [Proc. of the Int. Conf. “Information means and technologies”]. Moscow, 1996, 9 p.

8. Korablin Yu.P. Semantika yazykov programmirovaniya [Programming Language Semantics]. Moscow, MEI Publ., 1992, 100 p.

9. Korablin Yu.P., Kosakyan M.L. Analysis of the asynchronous functional schemes program models using linear-time temporal logic. Programmnyeprodukty i sistemy [Software & Systems]. 2014, no. 2 (106), pp. 5-10 (in Russ.).

10. Alagich S., Arbib M. Proektirovanie korrektnykh strukturirovannykhprogramm [Valid Structured Programs Design]. Moscow, Radio i svyaz Publ., 1979, 292 p.

11. Hoare C.A.R. An Axiomatic Basis for Computer Programming. N.Ireland, Queen's Univ. of Belfast Publ., 1969, pp. 576-580.

12. Abraham E., Havelund K. Tools and Algorithms for the Construction and Analysis of Systems. Springer Publ., 2014, 652 p.

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

179