автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.17, диссертация на тему:Алгоритмические свойства формальных моделей параллельных и распределенных систем

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

004607757

Кузьмин Егор Владимирович

АЛГОРИТМИЧЕСКИЕ СВОЙСТВА ФОРМАЛЬНЫХ МОДЕЛЕЙ ПАРАЛЛЕЛЬНЫХ И РАСПРЕДЕЛЕННЫХ СИСТЕМ

Специальность 05.13.17 — Теоретические основы информатики

АВТОРЕФЕРАТ - 2 СЕН 2010

диссертации на соискание ученой степени доктора физико-математических наук

Ярославль — 2010

004607757

Работа выполнена на кафедре теоретической информатики Ярославского государственного университета им. П. Г. Демидова.

Научный консультант:

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

Официальные оппоненты:

доктор физико-математических наук, доцент Дехтярь Михаил Иосифович

Ведущая организация:

Институт системного программирования РАН

Защита состоится 3 декабря 2010 г. в 13 час. на заседании диссертационного совета ДМ002.084.01 при Учреждении Российской академии наук Институте программных систем им. А. К. Айламазяна РАН, расположенном по адресу: 152021, Ярославская область, Переславский район, с. Веськово, ул. Петра I, д. 4а.

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

Автореферат разослан »аЛу/ЖШ^ 2010 г.

Ученый секретарь

диссертационного совета, к. т. н. номарева С. М.

доктор технических наук, профессор Карпов Юрий Глебович

доктор физико-математических наук, профессор Ломазова Ирина Александровна

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

Актуальность работы. Современный период развития информатики и вычислительной техники характеризуется широким использованием параллельных и распределенных систем (вычислительные машины и комплексы с параллельной и распределенной архитектурой, параллельные программы, протоколы передачи данных, модели технологических и бизнес-процессов), поведение которых отличается высокой степенью сложности. Это обстоятельство выдвигает новые задачи в области моделирования и анализа корректности таких систем. Под корректностью понимается полное соответствие системы задачам, для которых она создаётся. Корректность определяется абстрактным образом в соответствии с формальной спецификацией, описывающей желаемое поведение системы. Процесс проверки соответствия поведения системы требованиям, заданным в спецификации, называется верификацией.

За время исследований по проблеме верификации был разработан ряд методов проверки корректности параллельных и распределенных систем и накоплено большое количество теоретических результатов и практического опыта в этой области. Среди отечественных исследований по спецификации, моделированию и анализу распределенных систем отметим работы H.A. Анисимова, О.Л. Бандман, И.Б. Вирбицкайте, В.В. Воеводина, В. А. Захарова, Ю. Г. Карпова, В. Е. Котова, И. А. Ло-мазовой, В. А. Непомнящего, Р. Л. Смелянского, В. А. Соколова, Л. А. Черкасовой, Н. В. Шилова.

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

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

Для того чтобы преодолеть этот недостаток, были разработаны методы, применимые, по крайней мере, для некоторых ограниченных классов систем с бесконечным числом состояний. Можно упомянуть здесь работы, например, П. Абдуллы, К. Чёранса, А. Финкеля, Б. Йонссона, Ф. Моллера, Ф. Шнеблена. Более того, оказалось, что метод проверки модели, широко используемый при автоматической верификации систем с конечным числом состояний, может быть применен для некоторых классов систем с бесконечным числом состояний и подмножеств темпоральных логик.

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

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

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

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

Примерами других формальных моделей (систем переходов с бесконечным числом состояний), позволяющих описывать параллельные и распределенные системы, являются сети Петри, базовые параллельные процессы (ВРР — Basic Parallel Processes), системы с каналами, теряющими сообщения (LCS — Lossy Channel Systems), автоматы реального времени (Real-Time Automata) и др.

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

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

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

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

В качестве общего средства для демонстрации неразрешимых проблем для вполне структурированных систем переходов рассматриваются «слабые» счетчиковые машины. Абстрактная счетчиковая машина — довольно простой и удобный объект для исследования неразрешимых семантических и темпоральных свойств систем переходов. Большое количество формализмов, порождающих вполне структурированные системы переходов, с легкостью могут задавать поведение «слабых» счетчиковых машин. Но в то же время такие проблемы, как ограниченность и достижимость, для некоторых классов машин являются неразрешимыми. Поэтому все неразрешимые проблемы для того или иного класса «слабых» счетчиковых машин автоматически распространяются на вполне структурированные системы переходов (формальные модели), способные отображать поведение этих машин.

Абстрактные счетчиковые машины строятся с помощью различных ослаблений, например, (безусловного) недетерминизма переходов и отношения потери значений счетчиков, на основе счетчиковых машин Минского, которые являются равномощны-ми универсальным машинам Тьюринга. Отсюда неразрешимость исследуемой проблемы устанавливается методом сведения неразрешимой проблемы машины Минского к данной проблеме. Необходимо отметить, что, если исследуемое для конкретной модели свойство является неразрешимым для класса систем переходов, к которому принадлежит модель, это еще не означает бесполезность проверки его выполнимости. Поскольку доказательство

неразрешимости некоторого свойства проводится на одном «плохом» примере для всего класса систем переходов в целом, то в конкретном случае, в конкретной модели с учетом ее особенностей проверка свойства может привести к положительному (или отрицательному) результату, т. е. проверка свойства может быть осуществлена.

Ранее в ряде публикаций таких авторов, как А. Буаджа-ни, О. Буркарт, X. Эспарза, Р. Майр, исследовались вопросы разрешимости задачи проверки модели для некоторых конкретных представителей класса вполне структурированных систем переходов, а именно: магазинных автоматов, сетей Петри, ВРР, систем сложения векторов с потерями (LVAS) и различных темпоральных логик линейного времени и ветвящегося времени. В данной же работе, исходя из позиции обобщения, акцентируется внимание на проблеме разрешимости темпоральных свойств для различных классов вполне структурированных систем помеченных переходов, в частности, для нового класса вполне структурированных систем переходов автоматного типа, которые из-за своей специфической структуры можно также отнести и к классу систем переходов, независимых от данных.

В литературе практически не уделяется внимание системам переходов, независимых от данных (за исключением систем переходов с конечным числом состояний). Тем не менее, как будет показано в данной работе, системы, принадлежащие к этому классу, могут быть достаточно выразительными и нетривиальными. Для демонстрации этого факта в диссертации предлагается специальный фрагмент алгебры процессов, построенный на основе таких хорошо известных алгебр процессов, как CCS (Calculus of Communicating Systems — исчисление взаимодействующих систем) Милнера и SCP (Communicating Sequential Processes — взаимодействующие последовательные процессы) Хоара, позволяющий строить формальные модели (параллельных и распределенных систем), которые могут быть рассмотрены как независимые от данных помеченные системы переходов, а точнее, как вполне структурированные системы переходов автоматного типа.

В качестве примера конкретной реализации этого фрагмента в данной работе предлагается и исследуется формализм, названный «взаимодействующие раскрашивающие процессы» (ССР — Communicating Colouring Processes), позволяющий строить модели распределенных систем, где поведение каждого компонента описывается последовательным процессом и между ними организовано взаимодействие, направленное на обмен и передачу пакетов информации. Формализм ССР принимает во внимание факт передачи данных, а также позволяет отслеживать перемещение данных различного типа между компонентами системы. Но переход из одного состояния в другое не зависит от оперируемых данных, а определяется только управляющими состояниями.

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

Достижение цели связывается с решением следующих задач:

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

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

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

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

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

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

Методы исследования базируются на аппарате математической логики, теории квазипорядков и теории автоматов, языков и вычислений. В частности, при исследовании свойств систем переходов использовались теории программных и временных логик, семантики параллелизма, вполне структурированных систем помеченных переходов. При построении и анализе новых формализмов применялись теории счётчиковых машин, сетей Петри и алгебр процессов. Выделяются три основные направления исследований: структурированные системы переходов, счетчиковые машины, моделирование и анализ программных систем. В поддержку выделенных направлений автором были опубликованы соответственно монография «Вполне структурированные системы помеченных переходов» (в соавторстве с д. ф.-м. н., проф. В.А. Соколовым), учебные пособия «Счетчиковые машины» и «Верификация моделей программ».

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

Теоретическая и практическая значимость. Полученные результаты имеют в основном теоретический характер. Тем не менее, они могут быть использованы при решении практических задач верификации параллельных и распределённых систем (как с конечным, так и бесконечным числом состояний). Предложенный формализм взаимодействующих раскрашивающих процессов может быть использован как теоретическая основа для моделирования и анализа поведенческих свойств распределённых систем, в которых особое внимание уделяется отслеживанию перемещения данных различного типа среди их компонентов. Предложенная (на базе метода model checking) технология моделирования, спецификации и верификации программ, построенных на основе автоматного подхода к программированию, позволила создать программный комплекс «Система моделирования и анализа автоматных программ».

Основные результаты и положения.

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

2. Установлен ряд фактов, дополняющих теорию счетчико-вых машин. В частности, предложен способ моделирования трехсчетчиковых машин Минского с помощью двухсчет-чиковых при взаимно однозначном соответствии конфигураций вида (2iV3K5L,0) и (N,K,L). Доказано, что для двухсчетчиковых машин Минского проблемы ограниченности, ограниченности одного счетчика, остановки хотя бы при одном входе, достижимости заданной конфигурации не являются разрешимыми, но имеют частичный алгоритм решения, а проблемы пустоты, тотальности, существования зацикливающего входа, эквивалентности, неограниченного

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

Была улучшена оценка (с кубической до квадратичной от числа состояний машины) максимальной длины конечного представления бесконечного исполнения односчетчиковой машины Минского и предложен алгоритм нахождения границ этого представления с квадратичной от числа состояний временной оценкой.

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

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

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

Представлен специальный фрагмент алгебры процессов, определяемой в стиле CSP Хоара и CCS Милнера, позволяющий строить формальные модели (параллельных и

распределённых систем), которые могут быть рассмотрены как независимые от данных помеченные системы переходов, а более конкретно, вполне структурированные системы переходов автоматного типа.

Предложена конкретная реализация этого класса взаимодействующих процессов независимых от данных, новый формализм для моделирования распределённых систем, позволяющий отслеживать перемещение данных различного типа между компонентами системы, названный взаимодействующие раскрашивающие процессы (Communicating Colouring Processes — ССР).

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

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

6. Определен и исследован класс языков, допускаемых автоматными счетчиковыми машинами. Доказано, что этот класс замкнут относительно операций объединения, пересечения, конкатенации, бесконечной итерации, гомоморфизма и обратного гомоморфизма, т.е. является полным абстрактным семейством языков. Также установлено, что класс языков автоматных счетчиковых машин (ЯАСМ) замкнут относительно полной подстановки, но незамкнут относительно дополнения и операции обращения. Доказано,

что для класса ЯАСМ разрешимы проблемы пустоты и распознавания слова языка, заданного автоматной счетчиковой машиной, но неразрешимы проблемы включения и равенства языков. Проведено сравнение с другими классами языков — регулярными, контекстно-свободными, контекстно-зависимыми языками и языками сетей Петри. Установлено, что класс АСМ-языков включает в себя регулярные языки, несравним по включению с классом контекстно-свободных языков и классом языков сетей Петри, но полностью входит в класс контекстно-зависимых языков.

7. На базе метода проверки модели (model checking) предложена технология моделирования, спецификации и верификации «автоматных» программ.

Апробация работы. Результаты диссертации докладывались на Международном симпозиуме «Temporal Representation and Reasoning» (Tatihou, Франция, 2004), Международном рабочем совещании «Распределенные информационно-вычислительные ресурсы и математическое моделирование» (Новосибирск, 2004), Международном рабочем совещании «Program Understanding» (Новосибирск - Алтай, 2003, 2009), Всероссийской научной конференции, посвящённой 200-летию Ярославского государственного университета им. П.Г. Демидова (2003), Всероссийской научной конференции «Методы и средства обработки информации» (Москва, МГУ, 2005, 2009), Научно-методической конференции преподавателей математического факультета и факультета ИВТ ЯрГУ им. П. Г. Демидова (2007), семинаре «Go4IT — шаг к новым технологиям Интернета» (Москва, Институт системного программирования РАН, 2007), Областной научно-методической конференции (Ярославль, ЯрГУ, 2007), Международной научной конференции «Образование, наука и экономика в вузах. Интеграция в международное образовательное пространство» (Польша, Плоцк, 2008), Международной научно-практической конференции «Информационно-коммуникативная культура: наука и образование» (Ростов-на-Дону, 2009), Международной конференции «Компьютерные

науки и информационные технологии» (Саратов, 2009), Международном рабочем совещании «Program Semantics, Specification and Verification: Theory and Applications (PSSV 2010)» (Казань, 2010), семинаре «Моделирование и анализ информационных систем» кафедры теоретической информатики Ярославского государственного университета им. П.Г. Демидова (2001-2010).

Гранты. Работа по теме диссертации проводилась в соответствии с планами исследований по проектам, поддержанными следующими грантами: РФФИ №99-01-00-309 «Методы моделирования, анализа и верификации распределенных систем», №0301-00-804 «Разработка новых методов и средств моделирования и анализа процессов обработки информации в распределенных системах», №07-01-00702а «Разработка формальных моделей распределенных систем и исследование их семантических свойств», №05-07095008 (публикация монографии «Структурированные системы переходов»), Федеральная целевая программа «Интеграция», гранты ФАНИ №2007-4-1.4-18-02-041 «Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода» ФЦП «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007-2012 годы», №2009-1.1-113-050-013 «Разработка фундаментальных принципов и инновационных прикладных методов для моделирования, анализа и верификации информационных систем» ФЦП «Научные и научно-педагогические кадры инновационной России на 2009-2013 годы».

Авторские свидетельства. Свидетельство об официальной регистрации программы для ЭВМ «Система моделирования и анализа автоматных программ», Федеральная служба по интеллектуальной собственности, патентам и товарным знакам, №2007611856. Зарегистрировано в Реестре программ для ЭВМ 7 мая 2007 г. Правообладатель: Ярославский госуниверситет им. П.Г. Демидова. Авторы: Е.В. Кузьмин, P.A. Виноградов, В. А. Соколов.

Личный вклад. Выносимые на защиту результаты получены соискателем лично. В опубликованных совместных работах постановка и исследование задач осуществлялись совместными усилиями соавторов при непосредственном участии соискателя.

Публикации. Материалы диссертации опубликованы в 41 печатной работе, из них 11 статей в журналах из перечня ВАК, 9 статей в рецензируемых журналах, не вошедших в этот перечень, 13 статей в сборниках трудов конференций и 3 тезисов докладов, 4 учебных пособия (1 с грифом УМО) и 1 монография (изд-во «Физматлит»), Получено 1 свидетельство о регистрации программы для ЭВМ. Список публикаций приведен в конце автореферата.

Структура и объём работы. Диссертационная работа изложена на 345 страницах и состоит из введения, семи глав, заключения и списка литературы. Иллюстративный материал включает 67 рисунков. Список литературы состоит из 177 наименований.

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

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

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

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

В разделе 1.2 приводятся понятия и определения теории вполне структурированных систем помеченных переходов.

Система помеченных переходов — одна из наиболее распространенных моделей для описания поведения параллельных и распределенных систем.

Система помеченных переходов представляет собой набор LTS = (S, Т, —>, so). гДе S — множество состояний с элементами s0,s\,S2, • ■ -,Т — некоторый конечный алфавит пометок (множество имен действий), —> С (S х Т х S) — отношение перехода между состояниями системы, sq е S — начальное состояние системы.

Последовательное исполнение для LTS есть конечная или бесконечная цепочка переходов so si ^ S2 —>■ ■ ■где sq — начальное состояние системы.

Вполне структурированной системой переходов со свойством транзитивной совместимости по возрастанию (соот. по убыванию) называется система переходов LTS = (S,T, —so), дополненная отношением правильного квазипорядка < С S х S, транзитивно совместимым по возрастанию (соот. по убыванию) с отношением переходов —>, т. е. для любых состояний s ^ q\ и любого перехода s s' существует непустая последовательность переходов qx q2 qn-i —> qn такая, что s' ^ qn и 5 ^ qi

Vi < п (соот. для любых состояний si ^ q и любого перехода

t I

q q существует непустая последовательность переходов si —»

—> S2 ~> • • - —> sn-1 такая, что sn ^ q' и Si ^ qVi < п).

Вполне структурированной системой переходов со свойством сильной совместимости по возрастанию (соот. по убыванию) называется система переходов LTS = (S,T,—*,sq), дополненная отношением правильного квазипорядка ^С S х S, совместимым сильно по возрастанию (соот. по убыванию) с отношением переходов —т.е. для любых состояний s ^ q и любого перехода s s' существует переход q q' такой, что s' ^ q' (соот. для любых состояний s ^ q и любого перехода q —> q' существует переход sis' такой, что s' ^ q').

В разделе 1.3 рассматриваются примеры формализмов, модели в рамках которых представляют собой вполне структурированные системы переходов разных классов. Сети Петри (соот. с обнуляющими дугами) — как вполне структурированные системы переходов со строгой сильной (соот. с сильной) совместимостью по возрастанию. FIFO-канальные системы с ненадежными каналами в зависимости от того, могут ли каналы связи в любое время внезапно ошибочно порождать или терять сообщения, содержащиеся в них, рассматриваются как вполне структурированные системы переходов либо с транзитивной совместимостью по возрастанию, либо с транзитивной совместимостью по убыванию.

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

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

В разделе 1.4 исследуются темпоральные свойства структурированных систем переходов в общем.

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

Метод проверки модели, широко используемый при автоматической верификации систем с конечным числом состояний, может быть применен для некоторых классов систем с бесконечным числом состояний и подмножеств темпоральных логик. Ранее в ряде публикаций таких авторов, как А. Буаджани, О. Буркарт, X. Эспарза, Р. Майр, исследовались вопросы разрешимости задачи проверки модели для некоторых конкретных представителей класса вполне структурированных систем переходов, а именно: магазинных автоматов, сетей Петри, базовых параллельных процессов (Basic Parallel Processes), систем сложения векторов с потерями (Lossy Vector Addition Systems) и различных темпоральных логик линейного времени и ветвящегося времени.

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

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

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

В разделах 2.1 и 2.2 дается определение машины Тьюринга как формализации интуитивного понятия алгоритма. С точки зрения понятия «массовых алгоритмических проблем» обсуждаются разрешимые и неразрешимые проблемы для машин Тьюринга. Приводятся теоремы о неразрешимости проблем «остановки» и «зацикливания».

В разделе 2.3 описывается другой вид универсальных математических машин — счетчиковые машины Минского.

Счетчиковая машина Минского представляет собой конечный автомат, имеющий доступ к памяти в виде нескольких неограниченных счетчиков, значениями которых могут быть лишь целые неотрицательные числа. Над каждым счетчиком допустимы лишь две операции: безусловное увеличение на единицу и условное вычитание единицы (т. е. в случае, когда счетчик равен нулю, происходит переход в альтернативное состояние).

Счетчиковые машины были введены в работах М. Минского, получив название «программные машины».

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

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

В этом разделе автором предложен способ моделирования трехсчетчиковых машин Минского с помощью двухсчетчиковых при взаимно однозначном соответствии конфигураций вида (2м2>кЬь,0) и

Теорема 2.6. Для любой трехсчетчиковой машины Минского ЗсМ может быть построена моделирующая ее работу машина Минского с двумя счетчиками 2сМ такая, что конфигурация со значениями счетчиков и В = О машины 2сМ будет существовать тогда и только тогда, когда существует конфигурация cX = N,Y = KuZ = L машины ЗсМ.

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

В разделе 2.4 на основе «базовых» неразрешимых проблем остановки и зацикливания, которые двухсчетчиковые машины наследуют от машин Тьюринга, с помощью метода сведения доказывается неразрешимость ряда проблем для двухсчетчиковых машин Минского.

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

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

Раздел 2.5 приводятся преобразования Р. Шреппеля, которые позволяют представлять двухсчетчиковые машины Минского в виде однорегистровых машин.

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

Ранее была известна оценка |Q|3 (где |Q| — количество состояний) длины конечного представления бесконечного исполнения односчетчиковой машины. В этом разделе автором предложен алгоритм (максимально приближенный по структуре к способу описания функционирования самой счетчиковой машины) нахождения границ этого конечного представления с временной оценкой 0(\Q2\).

Также в разделе доказывается (теорема 2.28) полиномиальная разрешимость проблем тотальной ограниченности и тотальной остановки односчетчиковых машин Минского.

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

Здесь обобщаются результаты, связанные с неразрешимыми свойствами формальных моделей систем с потерями (например, FIFO-канальные системы с потерями, сети Петри с обнуляющими дугами), посредством счетчиковых машин с потерями (lossy

counter machines — LCM), у которых значения счетчиков могут внезапно уменьшаться. Основное внимание уделяется проблеме ограниченности. Эта проблема является одной из самых важных для теории формальных моделей, поскольку в случае разрешимости позволяет определять, является ли множество состояний модели системы конечным, что критично, например, для автоматического метода верификации model checking.

Наряду со счетчиковыми машинами с потерями с той же целью рассматриваются и счетчиковые машины с ошибками (или просто «слабые» счетчиковые машины), в рамках которых при тестировании счетчиков на нуль допускается неверное определение нуля. Такие машины легко моделируются, например, сетями Петри.

Счетчиковые машины обоих классов объединены общим названием «слабые счетчиковые машины» из-за их способности лишь слабо реализовывать вычислимые функции, т. е. из-за недетерминизма переходов слабые счетчиковые машины вычисляют значение некоторой функции f(xi,...,xn), останавливаясь с результатом в счетчике у, таким образом, что у ^ f(x\,.. .,хп).

В разделе 3.1 рассматриваются счетчиковые машины с потерями (lossy counter machines), т.е. машины со счетчиками, значения которых могут уменьшаться самопроизвольно в любое время. Эти машины слабее по выразительной мощности, чем машины Минского, и могут быть заданы (моделироваться) многими формальными системами, но в то же время счетчиковые машины с потерями имеют интересные свойства, которые по-прежнему остаются неразрешимыми.

Счетчиковые машины с потерями были введены Р. Майром в качестве общего средства для демонстрации неразрешимости ряда проблем для систем с потерями, например, проблемы верификации систем с ненадежными каналами (lossy FIFO-channel systems), задачи проверки модели для сетей Петри с потерями, некоторых проблем для сетей Петри с обнуляющими дугами и параметрических проблем таких, как справедливость для протоколов передачи данных.

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

Пункт 3.1.2 посвящен проблеме ограниченности для счетчиковых машин с потерями. Ранее в работе авторов К. Дуфур, П. Янкара и Ф. Шнеблена при исследовании свойств сетей Петри с обнуляющими дугами была показана неразрешимость проблемы ограниченности для трехсчетчиковых машин с обнулениями. В данном разделе автором производится обобщение этого результата на счетчиковые машины с произвольным отношением потери.

Теорема 3.2. Проблема ограниченности для трехсчетчиковых машин с потерями неразрешима.

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

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

В статье соискателя, на основе которой написан этот пункт, для доказательства разрешимости проблемы ограниченности для двухсчетчиковых машин с обнулениями был применен совершенно другой подход, ориентированный на исследование вычислительной мощности двухсчетчиковых машин, продиктованный работой Р. Шреппеля (см. раздел 2.5).

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

нулевое). Для класса этих машин доказывается неразрешимость проблем включения и эквивалентности (теоремы 3.6 и 3.7). Кроме того, доказывается неразрешимость проблемы достижимости для слабых четырехсчетчиковых машин с отношением обнуления (теорема 3.8).

Четвертая глава посвящена системам переходов, независимых от данных.

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

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

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

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

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

В алгебрах процессов, каковыми являются, например, CCS (Calculus of Communicating Systems — исчисление взаимодействующих систем) и CSP (Communicating Sequential Processes — взаимодействующие последовательные процессы) конструктивный подход играет важную роль: процесс в них описывается с указанием того, как он построен из меньших процессов.

В этом разделе представлен фрагмент алгебры процессов, определяемой в стиле CSP Хоара и CCS Милнера, позволяющий строить формальные модели (параллельных и распределенных систем), которые могут быть рассмотрены как независимые от данных системы помеченных переходов, а более конкретно как вполне структурированные системы переходов с сильной совместимостью по возрастанию и убыванию, т.е. автоматного типа (см. далее).

Более того, предлагается конкретная реализация этого класса систем переходов, формализм для моделирования распределенных систем, позволяющий отслеживать перемещение данных различного типа между компонентами системы, — взаимодействующие раскрашивающие процессы (Communicating Colouring Processes — ССР).

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

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

Модель распределенной системы, реализованная в рамках формализма ССР, представляет собой параллельную композицию взаимодействующих последовательных процессов, синхронизирующихся между собой посредством взаимодействия через общие переменные (каналы). Каждое действие процесса — это либо передача, либо прием значения некоторого выражения над переменными. Результатом вычисления такого выражения является мультимножество над типами (цветами) данных. Совершение действия ССР приводит к изменению значения (раскраски) переменной. Поэтому работа процессов интерпретируется как раскрашивание множеств переменных. В терминах раскрашивания могут быть адекватно выражены, например, свойства систем, связанные с информационной безопасностью.

Конечные автоматы, или конечные машины (Finite State Machines — FSM), широко используются для моделирования систем, где управляющий аспект является доминирующим. Конечные автоматы графически изображаются в виде помеченных ориентированных графов, где узлы представляют собой состояния, а дуги, помеченные метками действий, являются переходами по состояниям. Взаимодействующие автоматы — это расширение конечных автоматов с помощью параллелизма и взаимодействия между параллельными компонентами. Параллелизм достигается организацией конечных автоматов в параллельную композицию, где все автоматы работают одновременно. Параллельные автоматы могут синхронизироваться посредством переходов, имеющих одинаковые метки. Взаимодействующие автоматы используются только тогда, когда принимается в расчет лишь факт взаимодействия компонентов, например, факт передачи пакета данных без описания его типа или содержимого.

С другой стороны, существует много формализмов таких, как машины Тьюринга и счетчиковые машины, сети Петри, системы с ненадежными каналами, которые имеют семантическое расширение и производят манипуляции с данными. Модель в рамках этих формализмов состоит из системы переходов с конечным числом управляющих состояний (управляющая часть), работающая с потенциально бесконечным множеством £> значений данных. Состояние такой системы может быть представлено в виде пары (</,с?), где д — управляющее состояние, а й £ Б. Переход в управляющей части имеет метку и операцию над множеством £). Переход возможен лишь в том случае, если будет истинен соответствующий этому переходу некоторый предикат над Б (т.е. переход зависит как от управляющих состояний, так и от данных, с которыми производятся манипуляции).

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

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

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

Теорема 4.2. Класс вполне структурированных систем переходов с сильной совместимостью по возрастанию и убыванию совпадает с классом вполне структурированных систем переходов автоматного типа.

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

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

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

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

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

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

Исследуются автоматные счетчиковые машины малой размерности, т.е. машины с одним, двумя и тремя счетчиками, и другими ограничениями.

В разделе 5.1 вводятся автоматные счетчиковые машины.

В разделе 5.2 доказывается (теорема 5.2) неразрешимость проблемы ограниченности автоматных трехсчетчиковых машин.

В разделе 5.3 доказывается (теоремы 5.3 и 5.4) неразрешимость проблем включения и эквивалентности для автоматных счетчиковых машин.

В разделе 5.4 доказывается разрешимость задачи достижимости некоторой нулевой конфигурации для всего класса автоматных счетчиковых машин (теорема 5.5). А также доказывается (теорема 5.6), что для автоматных четырехсчетчиковых машин проблема достижимости ненулевого вектора значений счетчиков является неразрешимой.

Раздел 5.5 посвящен автоматным счетчиковым машинам малой размерности.

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

Известно, что для 2-мерных систем векторного сложения с состояниями (сетей Петри, среди позиций которых неограниченными являются только две) и некоторых их расширений (с помощью добавлений обнуляющих, тестирующих на ноль и переме-

щающих значения счетчиков переходов) классические проблемы эквивалентности, включения и достижимости являются алгоритмически разрешимыми. Например, алгоритмы, представленные в работах Дж. Хопкрофта, Ж.-Ж. Пансио, Г. Сютре и А. Финкеля, производят построение множеств достижимых конфигураций, которые в случае двух счетчиков (двух неограниченных позиций) представляют собой полулинейные множества, имеющие конечное представление. Таким образом, каждая из указанных проблем может быть легко задана формулой арифметики Прес-бургера на основе полученного конечного представления множества достижимости. Известно, что арифметика Пресбургера разрешима, т. е. существует алгоритм определения истинности любой ее формулы.

Применение подобных алгоритмов ограничивается случаем абстрактных машин с двумя счетчиками, поскольку уже для «слабых» машин с тремя счетчиками, например 3-мерных систем векторного сложения с состояниями (сетей Петри с тремя неограниченными позициями), множество достижимых конфигураций не является полулинейным.

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

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

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

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

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

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

Ранее в статье А. Финкеля изучался специальный класс расширенных п-счетчиковых машин с ограничением на количество перемен направлений роста/убывания значений счетчиков. В ней было показано, что множество достижимости машин этого класса представляет собой полулинейное множество. Поскольку, очевидно, этот класс машин включает в себя класс автоматных счетчиковых машин с ограничением на количество перемен направлений роста/убывания значений счетчиков, то все положительные результаты (в том числе про полулинейность множества достижимости) могут быть распространены и на последний подкласс счетчиковых машин. Однако в работах О. Ибарры и А. Финкеля было доказано, что проблема определения, является ли произвольная п-счетчиковая машина Минского ограниченной по числу перемен направлений роста/убывания значений счетчиков, неразрешима. В них утверждается, что, например, для систем векторного сложения с состояниями указанная проблема разрешима. Является ли разрешимой эта задача для произвольной автоматной счетчиковой машины — открытая проблема. Из работ А. Финкеля и Д. Леру фактически следует, что если граф управления некоторой автоматной п-счетчиковой машины не содержит вложенных циклов, т.е. автоматная счетчиковая машина является «плоской», то множество достижимости такой машины полулинейно.

Шестая глава посвящена языкам автоматных счетчиковых машин.

В этой главе изучается класс языков, которые допускаются автоматными счетчиковыми машинами. Доказывается, что этот класс замкнут относительно операций объединения, пересечения, конкатенации, бесконечной итерации, гомоморфизма и обратного гомоморфизма (теоремы 6.4-6.7 ). Отсюда следует, что он является полным абстрактным семейством языков со всеми вытекающими из этого свойствами. Более того, класс языков автоматных счетчиковых машин (ЯАСМ) замкнут относительно полной подстановки (теорема 6.8), но незамкнут относительно дополнения и операции обращения (теорема 6.9). Для класса ЯАСМ разрешимы проблемы пустоты и распознавания слова языка (теоремы 6.1 и 6.3), заданного автоматной счетчиковой машиной, но неразрешимы проблемы включения и равенства языков (теоремы 6.10 и 6.11). Проводится сравнение с другими классами языков — регулярными, контекстно-свободными, контекстно-зависимыми языками и языками сетей Петри. Показывается, что класс АСМ-языков включает в себя регулярные языки, несравним по включению с классом контекстно-свободных языков и классом языков сетей Петри, но полностью входит в класс контекстно-зависимых языков.

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

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

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

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

Интересным является тот факт, что к «автоматным» программам могут быть успешно применимы (в совокупности) все существующие методы анализа корректности (верификации) сложных систем: имитационное моделирование, тестирование, дедуктивный анализ и метод проверки модели.

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

Несмотря на то, что дедуктивный анализ представляется очень трудоёмким методом с сильной привязкой к семантике языка программирования, который не может быть полностью автоматизирован и лишен контроля эксперта, при желании, он вполне может быть применим для «автоматных» программ после их полного построения, непосредственно для проверки корректности процедур (написанных на некотором языке высокого уровня), соответствующих выходным воздействиям или входным

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

С другой стороны для проверки логики «автоматных» программ удобным является метод проверки модели. При этом методе для программы строится формальная конечная модель (т. е. с конечным числом состояний), а проверяемые свойства задаются с помощью формул темпоральной логики. Проверка выполнимости темпоральных формул, задающих свойства модели, происходит автоматическим образом. Важно отметить, что построение модели программы для автоматической верификации является весьма серьёзной и сложной задачей. При построении модели для программы, написанной традиционным способом, возникает серьёзная проблема адекватности этой программной модели исходной программе. Модель может не учитывать ряд программных свойств или порождать несуществующие свойства. Автоматный подход к программированию с точки зрения моделирования и анализа программных систем имеет ряд преимуществ по сравнению с традиционным подходом. При автоматном программировании исключена проблема адекватности модели, поскольку набор взаимодействующих автоматов, описывающий логику программы, уже является адекватной моделью, по которой формальным образом строится программный модуль. И это является бесспорным плюсом автоматной технологии. Более того, модель имеет конечное число состояний, что является необходимым на практике условием для успешной автоматической верификации, поскольку метод проверки на модели представляет собой переборный метод.

Одними из наиболее популярных темпоральных логик для спецификации и верификации свойств программных систем являются логика CTL (branching-time logic или computation tree logic) и логика линейного времени LTL (linear-time logic). Для целей верификации автоматных программ логика LTL заслужи-

вает особого внимания, поскольку любая формула в рамках этой логики по сути представляет собой автомат Бюхи, описывающий (принимающий) бесконечные допустимые пути структуры Крип-ке, которая в свою очередь задаёт поведение (все возможные исполнения) проверяемой на корректность «автоматной» модели. Что позволяет при спецификации и верификации «автоматных» программ оперировать в основном таким простым понятием, как «автомат».

Таким образом, перечисленное выше позволяет говорить о возможности эффективного применения для верификации «автоматных» программ (для анализа корректности логики «автоматных» программ) метода проверки модели.

Существует ряд программных средств верификации абстрактных моделей, построенных в рамках некоторых формализмов (сети Петри, взаимодействующие асинхронные процессы, автоматы с реальным временем, гибридные автоматы и т.д.), базирующихся на общих подходах и технологиях. Среди этих средств верификации классическим методом проверки модели, можно выделить, например, CPNTools, SPIN, SMV и CADP, использующих в качестве языков спецификации формальных моделей соответственно раскрашенные сети Петри высокого уровня, язык Promela, синхронные процессы и язык LOTOS. С одной стороны, можно считать, что во многом целью создания такого рода программных продуктов является отработка тех или иных теоретических и прикладных методов верификации моделей, но в то же время, многие из них имеют ориентированный на конкретную область применения язык спецификации, например на моделирование и анализ коммуникационных протоколов или разработку синхронных аппаратных логических схем. Однако программных средств верификации, направленных непосредственно на поддержку технологии автоматного программирования, не существует, что не исключает, а скорее предполагает, активное использование уже имеющихся (проверенных временем) разработок ведущих лабораторий мира, которые обычно долгое время сопровождаются тематическими конференциями (зачастую полностью посвященными этим продуктам). Существующие средства-

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

В этой главе предлагается и исследуется одна из возможных моделей построения автоматных программ — иерархическая модель. Для спецификации и верификации автоматных программ, построенных по этой модели, предлагается технология применения метода проверки модели (метода model checking). Исследуется возможность спецификации (с точки зрения простоты и адекватности восприятия) структурных и семантических свойств автоматных программ с помощью темпоральной логики. При этом акцент в большей степени ставится на семантике автоматных программ, чем на структуре; в отличие от большого количества работ, где взаимодействующие автоматы (с различными расширениями) рассматриваются как некий абстрактный формализм, для которого на ряду с разрешимостью классических для теоретической информатики свойств оценивается лишь трудоёмкость метода проверки модели, связанная только со структу-

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

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

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

Разделы 7.6 и 7.7 являются вспомогательными. В них дается синтаксис и семантика темпоральных логик ЬТЬ и СТЬ.

В разделе 7.8 рассматриваются типичные темпоральные свойства моделей автоматных программ.

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

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

В данном случае возможно осуществление редукции (уменьшения) введённой структуры Крипке автоматной модели относительно проверяемых темпоральных свойств, заданных формулами логик СТЬ и ЬТЬ.

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

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

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

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

Раздел 7.13 рассматриваются перспективы использования метода формальных утверждений о трассах как средства спецификации «автоматных» программ.

В заключении к главе (раздел 7.14) отмечается, что автоматная программа является исключительно удобным объектом для верификации методом проверки модели. Свойства программной системы в виде автоматов формулируются и специфицируются естественным и понятным образом, легко соотносятся со взаимодействующими автоматами, которые задают логику «автоматной» программы, так как элементами управляющих автоматов являются либо чётко выраженные состояния объекта управления, либо понятные действия над ним. Проверка свойств осуществляется в терминах, которые естественно вытекают из автоматной модели программы. Элементарные высказывания в рамках свойств определяются над элементами модели — событиями, входными и выходными воздействиями и состояниями. Если после верификации методом проверки модели тестирование выявит ошибку, то вид этой ошибки скорее всего будет относиться к некорректной программной реализации выходных воздействий, а не к нарушению логики программы, что при исправлении не потребует глобальной перестройки «автоматной» программы (всё сведётся к локальным исправлениям внутри одной или нескольких отдельных обычно небольших процедур, корректность которых затем может быть доказана методом дедуктивного анализа). Разработка формальных методов и технологий моделирования,

спецификации и верификации автоматных программ и построения на этой базе интегрированного программного комплекса, позволит проектировать и реализовывать надёжные программные системы управления ответственными объектами. Для этого целесообразно использовать уже существующие пакеты прикладных программ-верификаторов, которые разрабатываются и поддерживаются ведущими зарубежными и российскими научными лабораториями и центрами. Большинство подобных программных средств верификации предоставляются бесплатно для проведения научно-исследовательских работ. Однако существуют и коммерческие версии программ-верификаторов, позволяющие использовать их для выполнения промышленных заказов как непосредственно, так и в комбинации с другими средствами верификации и анализа программ. Исследования в этом направлении привели к созданию прототипа программы верификации под названием «Система моделирования и анализа автоматных программ» (регистр, номер свидетельства: 2007611856; авторы: Кузьмин Е.В., Соколов В.А., Виноградов P.A.).

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

ПУБЛИКАЦИИ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

Статьи в журналах из перечня ВАК

1. Кузьмин Е. В., Чалый Д. Ю. О языках автоматных счетчи-ковых машин // Моделирование и анализ информационных систем, 2010. Т. 17, №2. 24 с. (лично автором - 12 с.)

2. Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. Проблемы ограниченности счетчиковых машин Минского // Программирование, 2010. Т. 36, №1. С. 3-10 (лично автором - 3 е.).

3. Кузьмин Е. В., Чалый Д. Ю. О множестве достижимости автоматных счетчиковых машин // Моделирование и анализ информационных систем, 2010. Т. 17, №1. С. 52-64 (лично автором - 7 е.).

4. Кузьмин Е. В., Чалый Д. Ю. О множестве достижимости автоматных трехсчетчиковых машин // Моделирование и анализ информационных систем, 2009. Т. 16, №3. С. 77-84 (лично автором - 4 е.).

5. Кузьмин Е. В., Чалый Д. Ю. Об одном классе счетчиковых машин // Моделирование и анализ информационных систем, 2009. Т. 16, №2. С. 75-82 (лично автором - 4 е.).

6. Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. Применение метода формальных утверждений о трассах для спецификации, построения и верификации автоматных программ // Программирование, 2009. Т. 35, №1. С. 1-17 (лично автором - 6 е.).

7. Кузьмин Е.В., Чалый Д. Ю. Алгоритмы для проблемы ограниченности счетчиковых машин // Моделирование и анализ информационных систем, 2008. Т. 15, №4. С. 42-55 (лично автором - 7 е.).

8. Кузьмин Е. В. Проблема ограниченности для счетчиковых машин с потерями // Моделирование и анализ информационных систем, 2008. Т. 15, №3. С. 14-27 (лично автором -14 е.).

9. Кузьмин Е.В., Соколов В. А., Чалый Д. Ю. Проблемы ограниченности счетчиковых машин Минского // Доклады Академии наук, 2008. Т. 421, №6. С. 741-743 (лично автором - 1 е.).

10. Кузьмин Е. В., Чалый Д. Ю. О разрешимости проблем ограниченности для счетчиковых машин Минского // Моделирование и анализ информационных систем, 2008. Т. 15, №1. С. 16-26 (лично автором - 6 е.).

11. Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и верификация «автоматных» программ // Программирование, 2008. Т. 34, №1. С. 1-23 (лично автором - 12 е.).

Работы, опубликованные в других журналах и сборниках

12. Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. О языках автоматных счетчиковых машин // Материалы Международного семинара «Семантика, спецификация и верификация программ: теория и приложения». Казань, 2010. С. 70-75 (лично автором - 2 е.).

13. Кузьмин Е.В. Счетчиковые машины. Ярославль: ЯрГУ, 2010. 128 с. (лично автором - 128 е.).

14. Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. Об одном формальном подходе к построению автоматных программ // Труды межд. конф. «Компьютерные науки и инф. технологии». Саратов, 2009. С. 239-240 (лично автором - 1 е.).

15. Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. Автоматные счетчиковые машины // Сборник статей международной научно-практической конференции «Информационно-коммуникативная культура: наука и образование», Ростов-на-Дону, 2009. С. 321-325 (лично автором - 2 е.).

16. Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. Формальное построение автоматных программ // Труды Третьей Всероссийской научной конференции «Методы и средства обработки информации». Москва, МГУ, 2009. С. 130-135 (лично автором - 2 е.).

17. Kuzmin Е. V., Sokolov V. A., Chaly D. Ju. Automaton Counter Machines // Proc. of Int. Workshop on Program Understanding (sat. of PSI'09), 2009. P. 1-4 (лично автором - 2 е.).

18. Кузьмин Е.В. Верификация моделей программ. Ярославль: ЯрГУ, 2008. 176 с. (лично автором - 176 е.).

19. Кузьмин Е. В., Соколов В. А., Чалый Д. Ю. Об одном классе алгоритмических проблем для машин Минского // Сборник материалов международной научной конференции «Образование, наука и экономика в вузах» Польша, Плоцк, 2008. С. 536-537 (лично автором - 1 е.).

20. Кузьмин Е.В., Виноградов P.A., Соколов В.А. Система моделирования и анализа автоматных программ. Свидетельство об офиц. per. программы для ЭВМ №2007611856. Федеральная служба по интеллектуальной собственности, патентам и товарным знакам, 2007.

21. Кузьмин Е. В. Верификация программ // Сборник мат. IX областной научно-методической конф. «Актуальные проблемы совершенствования подготовки специалистов в вузе». Ярославль, ЯрГУ, 2007. С. 18-21 (лич. автор. - 4 е.).

22. Кузьмин Е. В., Васильева К.А. Верификация автоматных программ с использованием LTL // Моделирование и анализ информационных систем, 2007. Т. 14, №1. С. 30-42 (лично автором - 6 е.).

23. Кузьмин Е. В., Соколов В. А. О некоторых подходах к верификации автоматных программ // Сборник докладов семинара «Go4IT — шаг к новым технологиям Интернета». Москва, Институт системного программирования, 2007. С. 43-48 (лично автором - 4 е.).

24. Кузьмин Е.В., Соколов В. А. О дисциплине специализации «Верификация программ» // Материалы II научно-методической конференции преподавателей математического факультета и факультета ИВТ «Преподавание математики и компьютерных наук в классическом университете». Ярославль, ЯрГУ, 2007. С. 91-101 (лично автором - 6 е.).

25. Кузьмин Е. В., Соколов В. А. О верификации «автоматных» программ // Сборник статей к 20-летию факультета ИВТ «Актуальные проблемы математики и информатики». Ярославль, ЯрГУ, 2007. С. 31-35 (лично автором - 3 е.).

26. Кузьмин Е. В., Соколов В. А. Структурированные системы переходов. М.: Физматлит, 2006. 178 с. (л. автор. - 6 п. л.).

27. Кузьмин Е. В. Введение в теорию вычислительных процессов и структур. ЯрГУ, 2006. 140 с. (л. автор. - 8 п. л.).

28. Кузьмин Е.В., Виноградов P.A., Соколов В.А. Верификация автоматных программ средствами CPN/Tools // Моделирование и анализ информационных систем, 2006. Т. 13, №2. С. 4-15 (лично автором - 4 е.).

29. Кузьмин Е. В. Иерархическая модель автоматных программ // Моделирование и анализ информационных систем, 2006. Т. 13, №1. С. 27-34 (лично автором - 8 е.).

30. Кузьмин Е. В., Соколов В. А. Вполне структурированные системы помеченных переходов. М.: Физматлит, 2005. 176 с. (лично автором - 6 п. л.).

31. Кузьмин Е. В., Соколов В. А. Исследование свойств класса вполне структурированных систем переходов // Труды Второй Всероссийской научной конференции «Методы и средства обработки информации». Москва, МГУ, 2005. С. 388-393 (лично автором - 4 е.).

32. Kouzmin Е. V., Shilov N. V., Sokolov V. A. Model Checking jti-Calculus in Well-Structured Transition Systems // Proc. of 11th International Symposium on Temporal Representation and Reasoning, Tatihou, France, IEEE Press, 2004. P. 152-155 (лично автором - 2 е.).

33. Kouzmin E. V., Shilov N. V., Sokolov V. A. Model Checking /i-Calculus in Well-Structured Transition Systems // Joint Bulletin of NCC & IIS, Comp. Science, Novosibirsk, 2004. №20. P. 97-107 (лично автором - 6 е.).

34. Кузьмин Е. В., Соколов В. А. Проверка модели для вполне структурированных систем переходов автоматного типа // Мат. Межд. семинара «Распределенные информационно-вычислительные ресурсы и математическое моделирование», Новосибирск, 2004. С. 73-85 (л. автор. - 7 е.).

35. Кузьмин Е. В., Соколов В. А. Взаимодействующие раскрашивающие процессы // Моделирование и анализ информационных систем, 2004. Т. 11, №2. С. 8-17 (л. автор. - 5 е.).

36. Кузьмин Е. В. О разрешимости задачи проверки модели для автоматной логики и вполне структурированных систем переходов автоматного типа // Моделирование и анализ информационных систем, 2004. Т. 11, №1. С. 8-17 (лично автором - 10 е.).

37. Kouzmin E.V., Sokolov V.A. Communicating Colouring Automata // Proc. of Int. Workshop on Program Understanding (sat. of PSI'03), 2003. P. 40-46 (лично автором - 4 е.).

38. Кузьмин Е. В., Соколов В. А. Проверка свойств вполне структурированных моделей // Мат. Всероссийской научной конференции, посвященной 200-летию Ярославского государственного университета им. П.Г. Демидова, 2003. С. 50-54 (лично автором - 3 е.).

39. Кузьмин Е. В. Недетерминированные счетчиковые машины // Моделирование и анализ информационных систем, 2003. Т. 10, №2. С. 41-49 (лично автором - 9 е.).

40. Кузьмин Е. В. О разрешимости задачи проверки модели для модального /¿-исчисления и некоторых классов вполне структурированных систем переходов // Моделирование и анализ информационных систем, 2003. Т. 10, №1. С. 50-55 (лично автором - 6 е.).

41. Кузьмин Е.В. Верификация графов потоков данных с использованием символьной проверки модели для CTL // Моделирование и анализ информационных систем, 2001. Т. 8, №1. С. 38-43 (лично автором - 6 е.).

42. Кузьмин Е. В., Рубцов С. А. Модели и инструментальные средства для разработки и анализа графов потоков данных // Материалы межвузовской научно-технической конференции «Управляющие и вычислительные системы», Вологда, ВоГТУ, 2000. С. 96-97 (лично автором - 1 е.).

Подписано в печать 28.07.2010. Формат 60x84/16. Бумага офсетная. Отпечатано на ризографе. Тираж 100 экз. Заказ 29/10. Отдел оперативной полиграфии ЯрГУ 150000, г. Ярославль, ул. Советская, 14

Государственное образовательное учреждение высшего профессионального образования Ярославский государственный университет им. П. Г. Демидова

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

05201151437

Кузьмин Егор Владимирович

Алгоритмические свойства формальных моделей параллельных и распределенных систем

05.13.17 - Теоретические основы информатики

ДИССЕРТАЦИЯ на соискание ученой степени доктора физико-математических наук

Научный консультант

доктор физ.-мат. наук, профессор

Соколов Валерий Анатольевич

Ярославль - 2010

Содержание

Введение ......................................................................5

Глава 1. Структурированные системы помеченных переходов 15

1.1. Мультимножество и квазипорядок.................15

1.2. Структурированные системы помеченных переходов......20

1.2.1. Системы помеченных переходов..............20

1.2.2. Структурированные системы помеченных переходов . . 22

1.2.3. Метод насыщения......................23

1.2.4. Покрывающее дерево системы переходов.........28

1.2.5. Совместимость по убыванию................32

Глава 2. Автоматные структурированные системы переходов 35

2.1. Определение.............................36

2.2. Семантические свойства ......................36

2.3. Темпоральные свойства.......................40

2.4. Заключение к главе.........................52

Глава 3. Взаимодействующие раскрашивающие процессы ... 55

3.1. Взаимодействующие процессы, независимые от данных.....58

3.2. Взаимодействующие раскрашивающие процессы.........63

3.3. Заключение к главе.........................73

Глава 4. Счетчиковые машины Минского.............75

4.1. Счетчиковые машины Минского..................75

4.2. Двухсчетчиковые машины.....................84

4.2.1. Неразрешимые проблемы..................85

4.2.2. Проблема достижимости..................92

4.2.3. Проблемы ограниченности.................94

4.3. Однорегистровые машины.....................99

4.4. Односчетчиковые машины.....................111

4.4.1. Односчетчиковые машины.................112

4.4.2. Свойства односчетчиковых машин ............113

4.4.3. Алгоритм представления исполнения...........115

4.4.4. Обоснование алгоритма и трудоемкость .........118

4.4.5. Проблемы тотальности...................124

4.5. Заключение к главе.........................127

Глава 5. Слабые счетчиковые машины...............129

5.1. Счетчиковые машины с потерями.................130

5.1.1. Отношения потери.....................131

5.1.2. Ограниченность для счетчиковых машин с потерями . .133

5.1.3. Ограниченность для двухсчетчиковых машин

с обнулениями........................135

5.2. Слабые счетчиковые машины ...................147

5.3. Заключение к главе.........................162

Глава 6. Автоматные счетчиковые машины............163

6.1. Автоматные счетчиковые машины.................164

6.2. Проблема ограниченности .....................168

6.3. Проблемы включения и эквивалентности.............170

6.4. Проблема достижимости......................172

6.5. Автоматные счетчиковые машины малой размерности.....175

6.5.1. Автоматная 3-счетчиковая машина с неполулинейным множеством достижимости.................178

6.5.2. Автоматные односчетчиковые машины..........183

6.6. Автоматные счетчиковые машины с ограничениями.......193

6.7. Заключение к главе.........................194

Глава 7. Языки автоматных счетчиковых машин........195

7.1. Автоматная счетчиковая машина-распознаватель........195

7.2. Основные теоремы по проблемам пустоты

и распознавания слов........................197

7.3. Свойства замкнутости........................203

7.4. Проблемы включения и равенства языков............212

Глава 8. Моделирование, спецификация и верификация «автоматных» программ...........................219

8.1. Введение...............................220

8.2. Иерархическая модель автоматных программ..........225

8.3. Автоматная модель системы управления кофеваркой......229

8.4. Спецификация и верификация автоматных моделей.......238

8.5. Структура Крипке автоматной модели..............240

8.6. Темпоральная логика LTL.....................249

8.7. Темпоральная логика CTL.....................251

8.8. Темпоральные свойства автоматных моделей...........254

8.9. Редукция модели ..........................258

8.10. Практическая реализация .....................261

8.11. Автоматные модели систем реального времени..........262

8.12. Применение метода формальных утверждений о трассах .... 269

8.13. Заключение к главе.........................289

Заключение..................................291

Литература..................................294

Введение

Актуальность работы. Современный период развития информатики и вычислительной техники характеризуется широким использованием параллельных и распределенных систем (вычислительные машины и комплексы с параллельной и, распределенной архитектурой, параллельные программы, протоколы передачи данных, модели технологических и бизнес-процессов), поведение которых отличается высокой степенью сложности. Это обстоятельство выдвигает новые задачи в области моделирования и анализа корректности таких систем. Под корректностью понимается полное соответствие системы задачам, для которых она создаётся. Корректность определяется абстрактным образом в соответствии с формальной спецификацией, описывающей желаемое поведение системы. Процесс проверки соответствия поведения системы требованиям, заданным в спецификации, называется верификацией [14, 18, 22, 65].

За время исследований по проблеме верификации был разработан ряд методов проверки корректности параллельных и распределенных систем и накоплено большое количество теоретических результатов и практического опыта в этой области. Среди отечественных исследований по спецификации, моделированию и анализу распределенных систем отметим работы Н. А. Ани-симова, О. Л. Бандман, И. Б. Вирбицкайте, В. В. Воеводина, М.И. Дехтяря, В. А. Захарова, Ю. Г. Карпова, В.Е. Котова, И. А. Ломазовой, В. А. Непомнящего, Р. Л. Смелянского, В. А. Соколова, Л. А. Черкасовой, Н. В. Шилова.

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

Многочисленные методы и средства анализа параллельных и распреде-

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

Для того чтобы преодолеть этот недостаток, были разработаны методы, применимые, по крайней мере, для некоторых ограниченных классов систем с бесконечным числом состояний. Можно упомянуть здесь работы, например, П. Абдуллы, К. Чёранса, А. Финкеля, Б. Йонссона, Ф. Моллера, Ф. Шнебле-на [79, 115, 152]. Более того, оказалось, что метод проверки модели, широко используемый при автоматической верификации систем с конечным числом состояний, может быть применен для некоторых классов систем с бесконечным числом состояний и подмножеств темпоральных логик [92, 93, 110-112].

Проверка модели (model checking) — один из подходов к решению проблемы верификации [14, 18, 22]. В качестве языков спецификации для выражения свойств систем при этом подходе используются темпоральные логики. Задача проверки модели состоит в определении выполнимости для системы, заданной формальным образом (в виде формальной модели), свойства, представленного формулой темпоральной логики.

Исследования систем переходов с бесконечным числом состояний были мотивированы теорией формальных языков и грамматик [15, 71]. Во-первых, в этой теории бесконечные языки описываются грамматиками (т.е. имеют конечное представление), а во-вторых, некоторые проблемы для языков, например, проблема равенства регулярных языков, являются разрешимыми. Следовательно, не все проблемы систем переходов с бесконечным числом состояний неразрешимы. По аналогии с теорией формальных языков были вве-

дены новые формализмы для описания бесконечных систем переходов. ' Примерами формальных моделей (систем переходов с бесконечным чис-

лом состояний), позволяющих описывать параллельные и распределенные си-1 стемы, являются сети Петри [19, 66], базовые параллельные процессы (ВРР —

Basic Parallel Processes) [97], системы с каналами, теряющими сообщения « (LCS — Lossy Channel Systems) [80, 81], автоматы реального времени (Real-

Time Automata) [84] и др.

Указанные формализмы, как и многие другие, могут быть рассмотрены как вполне структурированные системы помеченных переходов [79, 115].

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

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

<

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

В качестве общего средства для демонстрации неразрешимых проблем для вполне структурированных систем переходов рассматриваются «слабые» счетчиковые машины. Абстрактная счетчиковая машина — довольно простой и удобный объект для исследования неразрешимых семантических и темпоральных свойств систем переходов. Большое количество «формализмов, порождающих вполне структурированные системы переходов, с легкостью могут задавать поведение «слабых» счетчиковых машин. Но в то же время такие проблемы, как ограниченность и достижимость, для некоторых классов машин являются неразрешимыми. Поэтому все неразрешимые проблемы для того или иного класса «слабых» счетчиковых машин автоматически распространяются на вполне структурированные системы переходов (формальные модели), способные отображать поведение этих машин.

Абстрактные счетчиковые машины строятся с помощью различных ослаблений, например, (безусловного) недетерминизма переходов и отношения потери значений счетчиков, на основе счетчиковых машин Минского, которые являются равномощными машинам Тьюринга. Отсюда неразрешимость исследуемой проблемы устанавливается методом сведения неразрешимой проблемы машины Минского к данной проблеме.

Ранее в ряде публикаций таких авторов, как А. Буаджани, О. Буркарт, X. Эспарза, Р. Майр [92, 93, 110, 112], исследовались вопросы применимости метода проверки модели для некоторых формализмов, модели в рамках которых могут быть рассмотрены как вполне структурированные системы переходов, а именно: сетей Петри, ВРР, систем сложения векторов с потерями (ЬУАБ). В данной же работе, исходя из позиции обобщения, акцентируется внимание на проблеме разрешимости темпоральных свойств для класса вполне структурированных систем помеченных переходов в целом.

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

класс автоматных структурированных систем переходов, особенностью которого является одновременное выполнение свойств совместимости по возрастанию и совместимости по убыванию правильного квазипорядка с отношением переходов. В литературе практически не уделяется внимание системам переходов этого класса (за исключением систем переходов с конечным числом состояний). Тем не менее, как будет показано в данной работе, формализмы, порождающие автоматные структурирвоанные системы переходов могут быть достаточно выразительными и нетривиальными. Для демонстрации этого факта в диссертации предлагается специальный фрагмент алгебры процессов, построенный на основе таких хорошо известных алгебр процессов, как CCS (Calculus of Communicating Systems — исчисление взаимодействующих систем) Милнера [151] и SCP (Communicating Sequential Processes — взаимодействующие последовательные процессы) Хоара [129], позволяющий строить формальные модели (параллельных и распределенных систем), которые могут быть рассмотрены как автоматные структурированные системы переходов.

В качестве примера конкретной реализации этого фрагмента в данной работе предлагается и исследуется формализм, названный «взаимодействующие раскрашивающие процессы» (ССР — Communicating Colouring Processes), позволяющий строить модели распределенных систем, где поведение каждого компонента описывается последовательным процессом и между ними организовано взаимодействие, направленное на обмен и передачу пакетов информации. Формализм ССР принимает во внимание факт передачи данных, а также позволяет отслеживать перемещение данных различного типа между компонентами системы. Но переход из одного состояния в другое не зависит от данных, над которыми совершаются операции, а определяется только управляющими состояниями.

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

Достижение цели связывается с решением следующих задач:

1. Упорядочение теории вполне структурированных систем помеченных переходов и дополнение ее общими результатами о разрешимости темпоральных свойств для различных классов структурированных систем переходов. Выявление и изучение новых классов систем переходов.

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

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

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

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

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

Методы исследования базируются на аппарате математической логики, теории квазипорядков, теории алгоритмов и теории автоматов, языков и вычислений. В частности, при исследовании свойств систем переходов использовались теории программных и временных логик, семантики параллелизма, вполне структурированных систем помеченных переходов. При построении и анализе новых формализмов применялись теории счётчиковых машин, сетей Петри и алгебр процессов. Выделяются три основные направления исследований: структурированные системы переходов, счетчиковые машины,,моделирование и анализ программных систем. В поддержку выделенных направлений автором были опубликованы соответственно монография «Вполне структурированные системы помеченных переходов» (в соавторстве с д. ф.-м. н., проф. В. А. Соколовым), учебные пособия «Счетчиковые машины» и «Верификация моделей программ».

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

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

и распределённых систем (как с конечным, так и бесконечным числом состояний). Предложен