авторефераты диссертаций БЕСПЛАТНАЯ  БИБЛИОТЕКА

АВТОРЕФЕРАТЫ КАНДИДАТСКИХ, ДОКТОРСКИХ ДИССЕРТАЦИЙ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ

Методы спецификации и верификации параллельных моделей с непрерывным временем

Российская академия наук

Сибирское отделение

Институт систем информатики

им. А.П.Ершова

На правах рукописи

Покозий Екатерина Александровна

МЕТОДЫ СПЕЦИФИКАЦИИ И ВЕРИФИКАЦИИ

ПАРАЛЛЕЛЬНЫХ МОДЕЛЕЙ С НЕПРЕРЫВНЫМ

ВРЕМЕНЕМ

05.13.11 — математическое и программное обеспечение

вычислительных машин, комплексов, систем и сетей

Автореферат диссертации на соискание ученой степени кандидата физико-математических наук Новосибирск, 1999

Работа выполнена в Институте систем информатики Сибирского отделения Российской академии наук

Научный руководитель: кандидат физико-математических наук, Вирбицкайте И.Б.

Официальные оппоненты: доктор технических наук, Бандман О.Л.

кандидат физико-математических наук, Соколов В.А.

Ведущая организация: Томский политехнический университет

Защита состоится 7 июня 1999 года в 14 час. 30 мин. на заседании дис сертационного совета К0003.93.01 в Институте систем информатики Си бирского отделения РАН по адресу:

630090, г.Новосибирск, пр. Лаврентьева, 6.

С диссертацией можно ознакомится в читальном зале библиотеки ВЦ СО РАН (пр. Лаврентьева, 6).

Автореферат разослан “_” апреля 1999 г.

Ученый секретарь специализированного совета К0003.93. к.ф.-м.н. М.А.Бульонков

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

синхронные/асинхронные, с глобальным/локальным временем, интер ливинговые/“истинно” параллельные, соотношением между действиями и временем (действия с нулевыми задержками).

Среди наиболее популярных формализмов систем реального вре мени встречаются как интерливинговые модели: временные автоматы, временные системы переходов, алгебры временных процессов, так и мо дели “истинного параллелизма”: временные структуры событий, времен ные причинно-следственные структуры, временные и стохастические се ти Петри.

Темпоральные логики являются удобным формализмом для специ фикации и верификации свойств параллельных и распределенных си стем. В данной проблематике сформировалось два подхода: аксиома тический и алгоритмический. При первом подходе разрабатывается си стема аксиом, с помощью которой может быть описана как сама си стема, так и ее свойства. Для верификационных целей используется механический доказыватель теорем. Основу второго подхода составля ют алгоритмы проверки на моделях (model checking), объединяющие в себе традиционные и логические методы анализа свойств параллель ных/распределенных систем. Основная цель исследований в этой обла сти состоит в том, чтобы сформулировать ясную логическую основу для создания автоматических систем верификации, синтеза и оптимизации параллельных систем.

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

Интересной задачей является верификация количественных свойств систем реального времени. Для выражения таких свойств удобно ис пользовать темпоральные логики реального времени. Р. Алюром был предложен алгоритм верификации свойств временных автоматов сред ствами темпоральной логики реального времени TCTL. Однако, при менение логик реального времени для верификации свойств временных сетей Петри остается открытым вопросом. Другая проблема верифи кации реальных систем состоит в том, что приходится анализировать огромное число состояний. Один из способов решения этой проблемы заключается в применении техники “частичных порядков”, которая поз воляет редуцировать число верифицируемых состояний за счет парал лелизма, присущего системе.

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



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

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

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

1. Разработка новых темпоральных языков реального времени с элементами параллелизма, позволяющих специфицировать и ве рифицировать поведение параллельных/распределенных систем реального времени.

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

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

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

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

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





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

• Предложена новая темпоральная логика реального времени, со держащая средства для описания свойств параллелизма в систе мах реального времени. Такая логика позволяет адекватно опи сывать системы, представленные моделями с семантикой “истин ного параллелизма”.

• Разработаны алгоритмы верификации поведенческих свойств раз личных временных сетевых моделей с использованием аппарата темпоральных логик реального времени.

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

Практическая ценность данных исследований состоит в возмож ности их использования при создании автоматизированных систем ве рификации систем реального времени. В частности, результаты диссер тационной работы использовались при создании модуля верификации в системе PEP (Programming Environment based on Petri nets), совместно разрабатываемой Институтом информатики Университета г. Хильдес хайма (Германия) и лабораторией теоретического программирования ИСИ СО РАН.

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

1. 4th Workshop on Logic, language, Information and Computation, Fortaleza (Ceara), Brazil, August 1997.

2. Distributed data processing (DDP’98), Novosibirsk, Russia, June 1998.

3. International Workshop on Discrete Event Systems (WODES’98), Cagliari, Italy, August 1998.

4. 1st International conference on practical and theoretical programming (UkrProg’98), Kiev, Ukraine. September 1998.

Кроме того, полученные результаты обсуждались на семинарах лабо ратории теоретического программирования ИСИ СО РАН и кафедры вычислительных систем НГУ.

Публикации. По теме диссертации опубликовано 9 научных работ.

Структура и объем работы. Диссертация состоит из введения, трех глав, заключения и списка литературы из 57 наименований. Основ ное содержание составляет 71 страницу. Работа включает 11 рисунков.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

В разделе 1.1 даются определения, связанные с понятием времен ной сети модели Мерлина.

Временная сеть N = (P, T, F, Ef t, Lf t, m0 ) характеризуется непере секающимися конечными множествами мест P и переходов T, отноше нием инцидентности F (P T ) (T P ), начальной разметкой m0 и целочисленными временными ограничениями: нижней (Ef t) и верхней (Lf t) временными границами, сопоставляемыми ее переходам. Ограни чимся рассмотрением однобезопасных временных сетей. Состоянием временной сети назовем пару, состоящую из разметки (множества мест, содержащих фишки) и множества вещественнозначных счетчиков, со поставленных с переходами. Во временной сети смена одного состоя ния другим осуществляется либо при истечении некоторого времени, либо при срабатывании некоторого перехода. Поведение временной се ти моделируется путями – последовательностями состояний, связанных срабатыванием переходов или истечением времени.

В разделе 1.2 приводятся синтаксис и семантика известной тем поральной логики реального времени TCTL, предложенной Р. Алюром.

Данная логика является расширением языка ветвящегося времени CTL за счет добавления временных ограничений на его операторы. Семан тика TCTL определяется на состояниях и путях временной сети. Будем говорить, что временная сеть N удовлетворяет TCTL-формуле, если выполняется в начальном состоянии N.

В разделе 1.3 разработан и исследован алгоритм, проверяющий, выполняется ли для временной сети некоторое свойство, заданное в виде TCTL-формулы.

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

Чтобы получить конечное представление сетевого поведения, введем понятие обобщенного состояния. Два состояния временной сети принад лежат одному и тому же обобщенному состоянию, если они в некотором смысле эквивалентны, то есть их разметки совпадают и значения соот ветствующих счетчиков согласованы по целым частям и порядку дроб ных частей. В качестве конечного представления поведения временной сети N при анализе TCTL-формулы строим граф обобщенных состоя ний G(N, ) с вершинами, соответствующими обобщенным состояниям и дугами, соответствующими срабатыванию переходов или истечению времени. Размер G(N, ) экспоненциален относительно размера N.

Алгоритм верификации TCTL-формулы на временной сети N со стоит в построении графа обобщенных состояний G(N, ) и пометке его вершин подформулами или их отрицанием. Чтобы проверить времен ные ограничения, встречающиеся в, для каждого ограничения c вводится новая элементарная формула pc, истинная тогда и только тогда, когда это ограничение выполнено. Алгоритм пометки вершины v подформулами рекурсивен. Для элементарных формул и логических связок пометка вершины v определяется естественным образом. Верши на v помечается формулой вида 1 Uc 2 (1 Uc 2 ), если в G(N, ) для любого пути, начинающегося в v (существует путь, начинающийся в v такой, что), его n-ая вершина помечена формулами 2 и pc для некоторого n 1, а все предшествующие ей вершины помечены фор мулой 1. Будем говорить, что временная сеть N удовлетворяет TCTL формуле, если и только если начальная вершина G(N, ) помечена.

Следующая лемма устанавливает корректность алгоритма пометки.

Лемма 1.3.4. Пусть — подформула TCTL-формулы. Предложен ный алгоритм помечает вершину v из G(N, ) формулой тогда и только тогда, когда выполняется на состоянии в N, принадлежащем v.

Далее дана оценка сложности предложенного алгоритма:

Теорема 1.3.2. Существует алгоритм, проверяющий, что временная сеть N удовлетворяет TCTL-формуле, который линеен по длине и размеру G(N, ) (и, следовательно, экспоненциален по размеру N ).

Введено понятие временной статтеринг-эквивалентности для графов обобщенных состояний, позволяющее осуществлять их корректную ре дукцию. Пусть даны временная сеть N и TCTL-формула. Будем гово рить, что место в N существенно для, если в существует элементар ная формула, соответствующая данному месту. Далее, будем говорить, что два графа обобщенных состояний G = G(N, ) и G = G(N, ) статтеринг-эквивалентны относительно TCTL-формулы, если на множествах их вершин определено отношение временной статтеринг эквивалентности:

1. начальные вершины G и G статтеринг-эквивалентны;

2. вершины v из G и v из G статтеринг-эквивалентны, если • их разметки на множестве мест, существенных для, сов падают и значения их счетчиков согласованы относительно временных ограничений из ;

• каждой дуге (v, v) из G соответствует конечный путь в G, в котором все вершины, кроме последней, статтеринг-экви валентны v, а последняя вершина статтеринг-эквивалентна v;

• аналогично предыдущему пункту, меняя местами G c G, а также v c v.

Теорема 1.3.1. Пусть графы обобщенных состояний G(N, ) и G(N, ) статтеринг-эквивалентны относительно TCTL-формулы. Далее, пусть v и v – вершины в G(N, ) и G(N, ) соответственно. Если вершины v и v статтеринг-эквивалентны, то v помечена формулой тогда и только тогда, когда v помечена формулой.

В разделе 1.4 описано использование техники “частичных поряд ков” для редукции числа анализируемых обобщенных состояний вре менной сети. Данный метод редукции использует тот факт, что многие свойства не ‘чувствительны’ к порядку, в каком выполняются парал лельные переходы временной сети, что позволяет избежать констру ирования эквивалентных состояний (то есть состояний, достижимых срабатыванием различных интерливинговых последовательностей пе реходов). Особенность предложенной редукции состоит в учете как па раллелизма сети, так и существенности временных ограничений при проверке выполнимости заданного свойства. Будем говорить, что в вер шине v графа обобщенных состояний G(N, ) время существенно для, если для некоторого временного ограничения c из время, соот ветствующее вершине v, не превышает c. Идея редукции состоит в сле дующем: для каждой вершины v строящегося редуцированного графа обобщенных состояний GR (N, ) при порождении следующих вершин рассматриваются не все срабатывающие переходы (как при построении G(N, )), а их подмножество и, кроме того, истечение времени, если в вершине v время существенно для. Показано, что редукционная про цедура полиномиальна по размеру временной сети.

Теорема 1.4.1. Для заданных временной сети N и TCTL-формулы графы обобщенных состояний G(N, ) и GR (N, ) статтеринг-эквива лентны.

Таким образом, алгоритм пометки для G(N, ) сводится к алгорит му пометки для GR (N, ).

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

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

В разделе 2.1. вводятся основные определения, касающиеся пара метрической временной сети и ее поведения.

Введем конечное множество параметров. Параметрическая времен ная сеть PN = (P, T, F,, m0 ) характеризуется непересекающимися ко нечными множествами мест P и переходов T, отношением инцидентно сти F (P T ) (T P ), начальной разметкой m0 и функцией, сопо ставляющей каждому переходу некоторый временной предикат, индук тивно определяющийся следующим образом: = f alse | x | 1 2, где – параметр или натуральное число, x – переход в PN, 1 и 2 – временные предикаты и — одно из бинарных отношений,, =,,.

Ограничимся рассмотрением однобезопасных параметрических времен ных сетей.

Вводится понятие означивания как функции, сопоставляющей каж дому параметру некоторое натуральное число. Означивание называется c-ограниченным для некоторого натурального числа c, если оно сопо ставляет каждому параметру значение, не превышающее c. Для задан ного означивания, обозначим параметрическую временную сеть PN с означенными посредством параметрами через PN. Будем называть означенной параметрическую временную сеть, все параметры которой означены посредством некоторого. Функционирование модели опре деляется для означенных параметрических временных сетей. Состояние означенной параметрической временной сети определяется аналогично состоянию временной сети, определенному в главе 1. Будем говорить, что переход t готов в состоянии q означенной параметрической времен ной сети PN, если в PN все входные места перехода t имеют фишки.

В означенной параметрической временной сети смена одного состояния другим осуществляется либо при истечении некоторого времени, либо при срабатывании некоторого перехода. Пусть q – состояние в PN. Бу дем говорить, что в состоянии q переход t T может сработать, если он готов в q и временной предикат (t) при означивании и подстанов ке вместо переходов соответствующих значений счетчиков – истинен.

Будем говорить, что в состоянии q может пройти время, если для всякого перехода t, готового в q, временной предикат (t) при озна чивании и подстановке вместо переходов соответствующих значений счетчиков будет истинен через некоторое время, не меньшее, чем.

В разделе 2.2 приведены синтаксис и семантика параметрической темпоральной логики реального времени PTCTL (Parametric Timed Computation Tree Logic), предложенной Ф. Вангом. PTCTL является расширением известной логики ветвящегося времени TCTL за счет вве дения параметрических переменных, представляющих неспецифициро ванные временные ограничения, в ее операторы. Семантика PTCTL определяется на состояниях и путях означенной параметрической вре менной сети. Для заданного означивания, обозначим PTCTL-формулу с означенными посредством параметрами через. Будем говорить, что параметрическая временная сеть PN удовлетворяет PTCTL-фор муле при означивании, если формула выполняется в начальном состоянии PN.

Задача c-ограниченного анализа параметрической временной сети PN относительно PTCTL-формулы состоит в нахождении c-ограни ченного означивания такого, что PN удовлетворяет формуле при означивании.

В разделе 2.3 строится конечное представление поведения парамет рической временной сети на основе понятия обобщенного состояния.

Для конечного представления поведения означенной параметриче ской временной сети PN при анализе PTCTL-формулы использу ется граф обобщенных состояний G(PN, ). c-ограниченный граф обобщенных состояний G(PN,, c) для параметрической временной се ти PN и PTCTL-формулы строится как объединение графов обоб щенных состояний G(PN, ) по всем c-ограниченным означиваниям. Для определения временной длительности путей в графе вводится понятие кактус-структуры, которая представляет собой набор простых циклов, связанных с некоторым простым путем. Данное понятие позво ляет выразить время произвольного пути в графе обобщенных состоя ний через времена простых путей и циклов.

В разделе 2.4 разрабатывается алгоритм решения задачи c-огра ниченного анализа параметрической временной сети PN относительно PTCTL-формулы, который заключается в построении графа обоб щенных состояний G(PN,, c) и пометке пары (v, ), где v – вершина G(PN,, c) и – подформула формулы, некоторой формулой логики первого порядка L(v, ), называемой условием, с параметрами в каче стве свободных переменных. Для c-ограниченного означивания, будем говорить, что является решением задачи c-ограниченного анализа па раметрической временной сети PN относительно PTCTL-формулы, если для начальной вершины v0 из G(PN,, c) означивание удовле творяет условию L(v0, ). Следующая теорема устанавливает коррект ность алгоритма пометки:

Теорема 2.4.1. Пусть даны задача c-ограниченного анализа парамет рической временной сети PN относительно PTCTL-формулы, – подформула, c-ограниченное означивание и вершина v в G(PN, ).

удовлетворяет условию L(v, ), тогда и только тогда, когда вы полняется на состоянии в PN, принадлежащем v.

Далее дана оценка сложности предложенного алгоритма:

Теорема 2.4.2. Существует алгоритм решения задачи c-ограниченно го анализа параметрической временной сети PN относительно PTCTL формулы, который линеен по размеру и дважды экспоненциален по размеру PN.

Третья глава посвящена введению новой темпоральной логики непре рывного времени с элементами параллелизма – TCCTL и ее использо ванию для спецификации и верификации поведения систем реального времени. Как и в главе 1 в качестве модели систем реального времени рассматриваются однобезопасные временные сети модели Мерлина.

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

В разделе 3.2 даются синтаксис и семантика новой темпораль ной логики реального времени TCCTL (Timed Concurrent Computation Tree Logic), которая является расширением языка ветвящегося времени CCTL, предложенного Пенчеком, за счет добавления временных огра ничений на его операторы. Специфику временной области удачно отра жает темпоральный оператор U ntil, позволяющий выражать свойства вида “формула 1 истинна до тех пор, пока не станет истинной форму ла 2 ”. Чтобы выражать свойства, связанные с параллелизмом, удобно использовать модификацию темпорального оператора N ext для логи ки непрерывного времени, которая позволяет выражать свойства вида “формула истинна после срабатывания произвольного перехода”. В TCCTL в качестве темпоральных операторов взяты операторы N ext (X) и U ntil (U) с явными временными границами.

Фиксируем временную сеть N. Множества state-формул и tree-фор мул определяются взаимно-индуктивно:

1. в качестве множества элементарных state-формул используется множество мест временной сети N ;

2. если 1 и 2 – state-формулы, то ¬1 и 1 2 – state-формулы;

3. если 1 и 2 – state-формулы, то AXc 1, EXc 1, A1 Uc 2, E1 Uc 2,– tree-формулы;

4. если 1 и 2 – tree-формулы, то ¬1 и 1 2 – tree-формулы;

5. если 1 – tree-формула, то 1 и 1 – state-формулы.

Здесь A, E – кванторы по путям, — одно из бинарных отношений,, =,,. State-формулы интерпретируются на состояниях вовре менной сети N, в то время как tree-формулы интерпретируются на под деревьях в N. Кванторы по поддеревьям позволяют выражать свойства, выполненные для всех (для некоторых, в зависимости от квантора) под деревьев с корнем в рассматриваемом состоянии. Будем говорить, что временная сеть N удовлетворяет state-формуле, если выполняется в начальном состоянии N.

В разделе 3.3 предложен алгоритм, проверяющий, выполняется ли для временной сети некоторое свойство, выраженное на языке TCCTL.

В качестве конечного представления поведения временной сети N при анализе state-формулы рассматривается структура обобщенных со стояний M(N, ), получающаяся в результате дискретизации множе ства поддеревьев в N. Размер M(N, ) экспоненциален относитель но размера N. Алгоритм верификации state-формулы на времен ной сети N состоит в построении структуры обобщенных состояний M(N, ) и пометке вершин M(N, ) state-подформулами формулы и дуг M(N, ) — tree-подформулами формулы. Идея алгоритма помет ки дуг состоит в следующем: дуга из M(N, ) помечается tree-формулой тогда и только тогда, когда она принадлежит некоторому поддере ву в M(N, ), на котором истинна. Для проверки истинности tree формулы на поддереве используется алгоритм, аналогичный алгоритму пометки, описанному в главе 1. В алгоритме пометки вершин наиболее сложным является случай формул с кванторами по поддеревьям. Вер шина v помечается state-формулой (), если в M(N, ) не существу ет дуги, помеченной tree-формулой ¬ (существует дуга, начинающаяся в v, помеченная tree-формулой ). Для случаев элементарных формул и логических связок пометка вершины определяется естественным об разом. Следующая теорема устанавливает корректность алгоритма по метки.

Теорема 3.3.1. Пусть — state-подформула формулы. Приведенный выше алгоритм помечает вершину v из M(N, ) формулой тогда и только тогда, когда выполняется на состоянии в N, принадлежащем v.

Далее дана оценка сложности предложенного алгоритма:

Теорема 3.3.2. Существует алгоритм, проверяющий, что временная сеть N удовлетворяет state-формуле, который линеен по размеру и полиномиален по размеру M(N, ), а, следовательно, экспоненциален по размеру N.

ОСНОВНЫЕ ВЫВОДЫ И РЕЗУЛЬТАТЫ В рамках диссертации были получены следующие результаты.

1. Разработан алгоритм верификации поведенческих свойств без опасных временных сетей на основе темпоральной логики реаль ного времени TCTL, который позволяет проверять не только ка чественные, но и количественные свойства сети.

• Построено конечное представление поведения сети в виде графа обобщенных состояний.

• Предложен алгоритм пометки графа обобщенных состояний TCTL-формулами.

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

• Введено понятие временной статтеринг-эквивалентности для обоснования корректности предложенной редукции.

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

2. Предложена новая модель систем реального времени — парамет рические временные сети.

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

• Понятие графа обобщенных состояний адаптировано к па раметрической природе временных ограничений.

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

3. Разработан метод верификации поведенческих свойств времен ных сетей с использованием аппарата темпорального языка ре ального ветвящегося времени TCCTL, который позволяет коли чественные свойства, связанные с параллелизмом системы.

• Введена и исследована новая темпоральная логика реаль ного времени TCCTL, содержащая средства для описания “истинного параллелизма” в системах реального времени.

• Предложено понятие поддеревьев на состояниях временной сети для характеристики параллельных выполнений систе мы.

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

• Предложен алгоритм анализа структуры обобщенных состо яний средствами TCCTL.

4. Дана оценка сложности предложенных алгоритмов и доказана их корректность.

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ 1. Вирбицкайте И.Б., Покозий Е.А., Использование техники частичных порядков для верификации временных сетей Петри.

Программирование, N 1, 1999, 28–41.

2. Вирбицкайте И.Б., Покозий Е.А., Метод параметрической верификации поведения временных сетей Петри. Программиро вание, N 4, 1999, 55–68.

3. Покозий Е.А., Поведенческий анализ параметрических времен ных сетей Петри. UkrProg’98 (1st International conference on practical and theoretical programming), сентябрь 1998, Киев, Украина, 111– 119.

4. Покозий Е.А., Метод верификации свойств параллелизма вре менных сетей Петри. Препринт 61, ИСИ, Новосибирск, 1999, стр.

5. Pokozy, E.A., Towards behaviour analysis of parametric time Petri nets. Proc. International Workshop on Discrete Event Systems (WODES’98), August 1998, Cagliari, Italy. The IEE Publisher, London, 1998, 517–518.

6. Pokozy, E.A., Behaviour analysis of parametric time Petri nets.

Joint Novosibirsk Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science, V. 9, Novosibirsk (1999), 73–89.

7. Virbitskaite, I.B., Pokozy, E.A., Model Checking of Time Petri Nets. Joint Novosibirsk Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science, V. 7, Novosibirsk (1997), 85–95.

8. Virbitskaite, I.B., Pokozy, E.A., Towards Ecient Verication of Time Petri Nets. Logical Journal of IGPL 5(6) Oxford University Press (1997) 921–924.

9. Virbitskaite, I.B., Pokozy, E.A., A partial order algorithm for verifying time Petri nets. Proc. International Workshop on Discrete Event Systems (WODES’98), August 1998, Cagliari, Italy. The IEE Publisher, London, 1998, 514–516.

Подписано в печать 28.04.99 Объем 1 уч.-изд.л.

Формат бумаги 6090 1/16 Тираж 100 экз.

Отпечатано на ризографе “AL-Group”.

630090, Новосибирск-90, пр. акад. Лаврентьева, 6.



 

Похожие работы:





 
2013 www.netess.ru - «Бесплатная библиотека авторефератов кандидатских и докторских диссертаций»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.