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

• Автор: Покозий, Екатерина Александровна
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 1999
• Место защиты: Новосибирск
• Количество страниц: 76 с. : ил.

Содержание
Введение
1 Метод верификации на основе темпоральной логики реального времени ТСТЬ
1.1 Определение временной сети
1.2 ТСТЬ: синтаксис и семантика
1.3 Алгоритм проверки на модели
1.4 Повышение эффективности путем использования частичных порядков
2 Метод параметрической верификации на
основе параметрической темпоральной логики реального времени РТСТЬ
2.1 Определение параметрической временной сети
2.2 РТСТЬ: синтаксис и семантика
2.3 Построение графа обобщенных состояний
2.4 Алгоритм поведенческого анализа
3 Метод верификации на основе параллельной темпоральной логики реального времени ТССТЬ
3.1 Построение древесной структуры состояний временной сети
3.2 ТССТЬ: синтаксис и семантика
3.3 Верификационный алгоритм
Заключение ТО
Литература

Введение
Актуальность проблемы. Параллельная обработка информации широко используется для увеличения производительности вычислительных систем. Особое место среди параллельных систем занимают системы реального времени, поведение которых в значительной степени зависит от количественных временных характеристик. Процесс проектирования систем такого типа — нетривиальная задача, требующая для своего решения фундаментальных исследований, основанных на различных формальных методах и средствах, которые варьируются в зависимости от класса моделируемых систем, степени детализации их структуры и поведения, а также от характера изучаемых проблем.
Для систем реального времени важны как модели времени, так и модели вычислений. Известны следующие дихотомии при задании временных характеристик: явное/неявное, линейное/ветвистое, ссылками на временные точки/интервалы, в непрерывной/дискретной временной области. Введение временных характеристик привело к появлению многих специализированных моделей вычислений с известными различиями: синхронные/асинхронные, с глобальным/локальным временем, интерливинговые/”истинно” параллельные, соотношением между действиями и временем (действия с нулевыми задержками).
Наиболее популярными среди формализмов систем реального времени являются как интерливинговые модели: временные автоматы [9], временные системы переходов [26], алгебры временных процессов [45], так и модели ’’истин-ного параллелизма”: временные структуры событий [29], временные причинно-следственные структуры [7], временные и стохастические сети Петри [33, 14, 46, 43, 57]. При интерливинговом подходе параллелизм событий моделируемой системы линеаризуется, то есть моделируется последовательной реализацией параллельных событий в произвольном недетерминированном порядке. Достоинством такого подхода является его простота и математическая элегантность. Однако параллелизм вычислений сводится к некоторой форме неде-терминизма. Альтернативный подход основывается на моделях с ’’истинным параллелизмом”, в которых все события изначально предполагаются независимыми. Отношение причинной зависимости между событиями задается частичным порядком, а отношение параллелизма - отсутствием такого порядка. Данные модели являются более приемлемыми для изучения таких свойств параллельных систем, как отсутствие тупиков, ’’справедливость”, максимальный параллелизм.
К достоинствам временных сетей Петри следует отнести удобное графическое представление, а также то, что благодаря семантике ’’истинного параллелизма” , данный формализм позволяет моделировать параллелизм системы есте-

ственным образом. Как правило, временные модели являются расширением традиционных моделей параллельных/распределенных систем за счет введения понятия времени. Так, временные сети Петри являются расширением сетей Петри [4], для которых существуют хорошо разработанные алгоритмы анализа поведенческих свойств [1].
Впервые временное расширение сетей Петри было предложено Рамхандани [43]. Существуют различные способы введения понятия времени в сеть Петри. Время может быть сопоставлено различным элементам сети Петри (местам, переходам, дугам, фишкам, шагам). При этом различают временные ограничения, которые сопоставляют некоторому элементу временной сети Петри фиксированную временную величину, и временные элементы - счетчики, контролирующие локальное или глобальное время. Временная информация может быть представлена как одним числом (что соответствует дискретному представлению времени), так и интервалом (что соответствует непрерывному представлению времени). В модели может предполагаться принуждение к срабатыванию переходов, то есть невозможность превышения заданных временных границ. Отдельным вопросом является наличие автопараллелизма в модели, а также возможность наличия в месте фишек с разными временными параметрами. В таблице 1 приведена информация о некоторых существующих моделях временных сетей Петри.
Темпоральные логики являются удобным формализмом для спецификации и верификации свойств параллельных и распределенных систем. В данной проблематике сформировалось два подхода: аксиоматический и алгоритмический. При первом подходе разрабатывается система аксиом, с помощью которой может быть описана как сама система, так и ее свойства [17]. Для верификационных целей используется механический доказыватель теорем. Основу второго подхода составляют алгоритмы проверки на моделях (model checking), объединяющие в себе традиционные и логические методы анализа свойств параллельных/распределенных систем [19]. Основная цель исследований в этой области состоит в том, чтобы сформулировать ясную логическую основу для создания автоматических систем верификации, синтеза и оптимизации параллельных систем.
Среди языков темпоральной логики, используемых для анализа параллельных систем различают логики линейного времени (linear-time) и логики ветвящегося времени (branching-time). Если представлять поведение системы в виде множества возможных последовательностей реализаций ее событий, то теряется информация не только о параллелизме, но также и о конфликтных событиях (недетерминированном выборе), то есть пропадает информация о ветвящейся структуре системы. Такой подход соответствует семантике линейного

2 Метод параметрической верификации на основе параметрической темпоральной логики реального времени РТСТЪ
Известно, что к временным сетевым моделям могут быть применены эффективные и довольно мощные верификационные алгоритмы (см., например, [15, 32, 56, 2]).
Одним из недостатков таких верификационных алгоритмов является то, что требуется детальная спецификация временных характеристик как системы, так и ее свойств. В случае если система не удовлетворяет заданному свойству, временные характеристики модифицируются, и вновь проверяется выполнимость свойства, что приводит к необходимости многократного исполнения верификационной процедуры. С целью преодоления такого рода трудностей в данной работе делается попытка ввести параметрические переменные в спецификацию временных характеристик как системы, так и ее свойства, что позволит осуществить их взаимную ‘настройку’ за однократное применение верификационного алгоритма. Для формального описания распределенных систем реального времени вводится понятие параметрической временной сети, которая является модификацией временной сети Петри [35, 56] за счет введения параметрических переменных в ограничения на время срабатывания переходов сети. Поведенческие свойства системы представляются в виде формул параметрической темпоральной логики реального времени РТСТЬ [55], которая изначально была введена для спецификации свойств временных автоматов. Суть предлагаемого верификационного алгоритма состоит в следующем. Сначала, используя понятие обобщенного состояния (аналога региона [8]), строится конечное графовое представление сетевого поведения (заметим, что параметрическая временная сеть базируется на модели непрерывного времени, и поэтому число ее состояний бесконечно). Процесс верификации состоит в нахождении условий (если таковые имеются) на значения временных параметров, при которых заданная логическая формула истинна на графе обобщенных состояний.
2.1 Определение параметрической временной сети
В этом пункте вводится ряд понятий, связанных с параметрической временной сетью и ее поведением. Под параметрической временной сетью понимается модификация временной сети Петри [35, 56] за счет введения параметрических переменных в ограничения на время срабатывания переходов сети.
Пусть N — множество натуральных чисел и 11+ — множество неотрица-