= ВОСЬМАЯ ЕРШОВСКАЯ КОНФЕРЕНЦИЯ ПО ИНФОРМАТИКЕ (ПСИ'11) =
УДК 681.3.06
МЕТОДЫ КОМПОЗИЦИИ ПРИ ПОСТРОЕНИИ ХАРАКТЕРИЗАЦИОННЫХ ФОРМУЛ ДЛЯ МОДЕЛЕЙ С НЕПРЕРЫВНЫМ ВРЕМЕНЕМ *
© 2012 г. Е. Н. Боженкова
Институт систем информатики СО РАН 630090 Новосибирск, пр. ак. Лаврентьева, 6 E-mail: bozhenko@iis.nsk.su Поступила в редакцию 30.11.2011
При верификации сложных вычислительных систем часто применяют понятия тестовой эквивалентности. Один из способов решения проблемы распознавания временных тестовых эквивалентностей в рамках модели временных структур событий с невидимыми действиями — сведение проблемы к проверке формулы на модели (model-checking). Для этого строятся логические формулы, характеризующие временную структуру событий с точностью до тестовых предпорядков. В статье рассматриваются методы композиции характеризиционных формул без использования графов регионов и классов, что упростит построение характеризационных формул.
1. ВВЕДЕНИЕ
Для упрощения структуры и повышения уровня абстракции при верификации и спецификации сложных систем, состоящих из большого числа взаимодействующих компонент, важным является понятие эквивалентности.
Понятие тестовой эквиваленности было предложено Хеннесси и де Николой в работе [1]. Два процесса считаются тестово эквивалентными, если они могут (may) или должны (must) проходить одинаковый набор тестов. Для облегчения применения тестовых эквивалентностей были найдены их альтернативные характери-зации для модели систем переходов. При этом внутренняя структура сравниваемых процессов предполагается известной, и сравнение проводится относительно множества всех возможных тестов. Тестовые эквивалентности используются для сравнения систем, проверки соответствия реализации ранее заданной спецификации, для проверки выполнимости логических формул.
Тестовые эквивалентности были исследованы для различных формальных моделей: для сис-
* Эта работа поддержана грантом DFG-РФФИ N 436 РФФИ 113/1002/01 и 09-01-91334.
тем переходов [1, 2], структур событий [3, 4], асинхронных моделей [5], для временных структур событий [6], временных сетей Петри [7], алгебр процессов [8, 9] с дискретным временем, временных автоматов [10]. Разрешимость тестовой эквивалентности обычно достигается ее сведением к бисимуляционной [2], для моделей с непрерывным временем показывается возможность дискретизации [7] или детерминиза-ции [10]. Нильсен и Скоу [10] предложили метод генерации конечного и полного множества тестов для для класса детерминизируемых временных автоматов с непрерывным временем. Фоглер и Бихлер [7] для асинхронной модели временных сетей Петри показывают возможность дискретизации, что позволяет получить совпадение тестовых отношений с дискретным и непрерывным временами.
Для модели временных структур событий с непрерывным временем тестовые отношения были исследованы в статьях [6], [11], [12]. В этой модели временные интервалы, сопоставленные событиям, обозначают временные рамки, когда событие должно случиться, после выполнения своих предшественников. Также предполагается, что выполнение события происходит мгновенно. В
[6] были найдены альтернативные характериза-ции тестовых предпорядков. Разрешимость тестовых отношений даётся через построение логической формулы [13], характеризующей временную структуру событий с точностью до тестовой эквивалентности. В качестве базовой логики использована временная модальная логика [14]. Характеризационная формула отражает структуру возможных выполнений временной структуры событий в удобном для анализа виде и строится с использованием графа регионов и графа классов. Для каждого класса строится своя формула, которая становится подформулой характеризационной формулы.
События различных компонентов системы могут взаимодействовать различными способами. Если события различных компонент находятся в одном и том же отношении — частичного порядка, конфликта или параллелизма — будем говорить, что система является композицией компонентов. В случае модели структур событий структура является композицией своих подструктур. Тогда интересно исследовать возможность построения характеризационных формул для всей структуры, используя только формулы подструктур, без дополнительных построений графов регионов и классов. Будем строить характеризационную формулу по известной схеме, используя формулы для классов подструктур.
Материал статьи разбит на части следующим образом. В гл. 2 вводятся основные понятия, связанные с временными структурами событий и временными тестовыми предпорядками и эквивалентностями. В гл. 3 даются понятия, используемые для получения конечного представления пространства состояний. Гл. 4 посвящена определению характеризационных формул. В гл. 5 рассматриваются методы композиции для построения характеризаци-онных формул. В Приложении приводится алгоритм дополнительных построений.
2. ВРЕМЕННЫЕ СТРУКТУРЫ СОБЫТИЙ
В этом разделе напоминаются основные понятия, связанные с моделью временных структур событий. Эта модель является расширением модели Винскеля [15] за счет
введения временных интервалов на события структуры.
Пусть Act — конечное множество действий и т — невидимое действие, причем т е Act, тогда ActT = Act U {т}.
Определение 1. Конечная структура событий, помеченная над ActT, — это набор S = (E, <,#, I), где E — конечное множество событий; < С E х E — частичный порядок (отношение причинной зависимости); # С E х E — симметричное и иррефлексивное отношение (отношение конфликта), удовлетворяющее принципу наследования конфликта: Ve, e', e" е E . e # e' < e" ^ e #e'' ; I : E ^ ActT — помечающая функция, сопоставляющая каждому событию из E действие из ActT.
Пусть S = (E, <, #,1) — структура событий. Для событий, не находящихся в отношениях причинной зависимости или конфликта, определим отношение параллелизма ^ как (E х E) \ (< U > U #). Множество C С E — левозам-кнутое, если событие содержится в множестве вместе со своими предшественниками: Ve, e' е E e е C Л e' < e ^ e' е C. Будем называть C бесконфликтным, если Ve, e' е C . —(e # e'). Конфигурацией в S назовем левозамкнутое и бесконфликтное множество. Множество всех конфигураций в S будем обозначать через Conf (S). Для C е Conf(S) определим множество готовых случиться событий следующим образом: En(C) = {e е E | C U {e} е Conf (S)}.
Для обозначения множеств натуральных и действительных чисел используются стандартные обозначения (N, R+, R+). Определим множество временных интервалов Interv(R+) = {[di,d2] с R+ | di < d2 е N}.
Теперь можем ввести понятие временной структуры событий.
Определение 2. Временная структура событий (ВСС), помеченная над ActT, — это пара TS = (S, D), где S = (E, <, #, I) — конечная структура событий, помеченная над ActT; D : E ^ Interv(R+) — временная функция, сопоставляющая каждому событию из E временной интервал из Interv(R+), такая, что D(e)) = [d, d] для некоторго d е No для всех e е E с 1(e) = т.
Временной интервал, приписываемый каждому событию, отражает отрезок времени, в который событие должно случиться.
Пример ВСС приведен на рис. 1. Множество событий ТБх — {ех, в2,ез, е4}. События в\, помеченное действием а, и ез, помеченное действием т, находятся в отношении конфликта, ез и е4 — в отношении причинной зависимости. Обычно имена событий опускаются и указываются только соответствующие помечающие действия.
Рис. 1.
Пример временной структуры событий.
Множество временных структур событий, помеченных над ЛсЬт, обозначим через Ет. Зафиксируем помеченные временные структуры событий ТБ = (Б = (Е, <,#,1),В) и ТБ' = (Б' = (Е', <', #', I'), В') из класса Ет.
ТБ называется конфликтно-свободной, если Е — бесконфликтное. ТБ' называется подструктурой ТБ, если Е' С Е, <'С<|Е, #' С # |Е, I' = I |Е, В' = В | Е.
Состоянием в ТБ называется пара М = (С, 6) такая, что С 6 Соп/(Б), 6 : Е А К+ — функция временных значений. Множество состояний в ТБ будем обозначать через БТ(ТБ). Пусть МТя = (0, 0) — начальное состояние в ТБ. Состояние М = (С, 6) называется заключительным,, если Еп(С) = 0.
Выполнение временной структуры событий представляется последовательностью переходов из состояния в состояние. Переход из одного состояния в другое осуществляется либо посредством выполнения события, либо посредством истечения некоторого времени. Событие готово выполниться в некотором состоянии, если бесконфликтное множество его предшественников уже выполнилось, а значение временной функции находится в пределах временного интервала, приписанного
данному событию. Предполагаем, что событие срабатывает мгновенно. В состоянии может пройти некоторое количество времени, если после этого временные значения готовых к выполнению событий не превысят границ временных интервалов.
Пусть Mi = (C1Л),M2 = (C2,82) е ST(TS), причем, Mi не является заключительным состоянием. Событие e е En(C1) может выполниться в M1 (обозначается M1 А, если 1(e) = a), если 81 (e) е D(e). Состояние M1 переходит в состояние M2 посредством выполнения события e (M1 А M2, если 1(e) = a), если M1 А, C2 = C1 U {e},
0, если e' е En(C2) \ En(C1) 81(e'), иначе. Время d е R+ может пройти в состоянии M1 (обозначается M1 А), если Ve е En(C1) 3d' > d . 81(e) + dd е D(e). Состояние M1 переходит в состояние M2 посредством истечения времени
d е R+ (обозначается M1 А M2), если C2 = C1, 82(e) = 81(e) + d для всех e е E.
Для того чтобы абстрагироваться от выполнения невидимых действий, будем использовать понятие слабого перехода. Слабое отношение перехода на состояниях в TS определяется как отношение = такое, что =2 А и =2
6X6 Т *
где А — рефлексивное транзитивное замыкание отношения А и x е Act U R+. Пред-
82(e') =
полагаем, что для отношения перехода
выпол-
d\ +d2
няется правило непрерывности времени: M
M == =2, где d1 ,d2 е R+.
Выполнение ВСС порождает язык ВСС, слова которого являются последовательностью временных действий.
Пусть Act(R+) = {a(d) | a е Act Л d е R+} — множество временных действий. Тогда (Act(R+ ))* — множество временных слов. Также пусть Л : (Act(R+ ))* А R+ — функция, измеряющая длительность временного слова, такая что: Л(е) = 0, Л('шм^
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.