Введение к работе
Актуальность. В настоящее время сфера применения аппаратных и программных систем с параллельной/распределенной архитектурой непрерывно расширяется, охватывая все новые области в самых различных отраслях науки, техники, образования, бизнеса и производства. К таким системам относятся коммуникационные протоколы, системы управления производством, распределенные операционные системы, параллельные базы данных и т.д. Параллельные/распределенные системы, как правило, состоят из большого числа компонентов со сложным характером взаимодействий, что затрудняет понимание природы протекающих в них разнообразных процессов. Проектирование и реализация корректных параллельных/распределенных систем возможны только при использовании формальных методов и средств, которые должны быть, с одной стороны, «дружественными» для разработчиков, а с другой - математически строгими, а также адекватно представлять структуру и поведение моделируемых систем.
Среди отечественных исследований по спецификации, моделированию и анализу сложных (в том числе, параллельных/распределенных) систем отметим работы И.А. Анисимова, О.Л. Бандман, И.Б. Вирбиц-кайте, В.В. Воеводина, Н.В. Евтушенко, В.А. Захарова, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.Э. Малышкина, В.А. Непомнящего, А.К. Петренко, Р.Л. Смелянского, В.А. Соколова, Л.А. Черкасовой.
Теория параллельных систем и процессов — активно развивающаяся область компьютерных наук - изучает фундаментальные понятия и законы параллельной обработки информации и на основе обнаруженных закономерностей строит более частные формальные модели исследуемых объектов, на которых ставит и решает прикладные задачи. На основе результатов и рекомендаций теоретических исследований ведется поиск и проверка новых архитектурных принципов конструирования систем, изучаются методы распараллеливания алгоритмов и программ, разрабатываются новые конструкции параллельных языков программирования, проверяются способы анализа и верификации программных систем и т.д. За последние четыре десятилетия в теории параллелизма появилось большое разнообразие моделей и методов, предназначенных
для спецификации, разработки и верификации систем. Среди формальных структурных моделей следует отметить сети Петри, системы переходов, системы переходов с независимостью, автоматы высших порядков, 1/О-автоматы и т.д. Особое внимание в теории параллелизма отводится абстрактным семантическим моделям, позволяющим описывать и исследовать поведения параллельных систем. К таким моделям относятся деревья синхронизации, причинные деревья, структуры событий и т.д. Известно, что денотационная семантика и теория областей Скотта активно используются как математический базис для описания семантики последовательных программ, установления взаимосвязей между языками программирования, исследования типов данных языков программирования. Примененимость таких абстрактных методов к моделям параллельных систем и процессов всегда вызывало некоторый скептицизм. Однако в работах Винскеля было показано, что модели областей Скотта адекватно и полностью представляют семантику известных моделей параллелизма.
Большое мнообразие моделей, предложенных в теории параллелизма, требует их систематизации и унификации. Последнее десятилетие методы теории категорий стали активно использоваться для описания, изучения и сравнительного анализа параллельных моделей. Основная идея подхода заключается в следующем. Объекты категорий представляют процессы, морфизмы соответствуют взаимосвязям между поведениями процессов. Тот факт, что одна модель более выразительна, чем другая, формально выражается в терминах вложений (или прообразов). На основе данного подхода были исследованы взаимосвязи между различными параллельными моделями: сетями Петри, сетями-процессами, структурами событий и областями Скотта; системами переходов с независимостью (высших порядков) и структурами событий (высших порядков), системами переходов с независимостью и асинхронными системами переходов; (асинхронными) системами переходов и сетями Петри; автоматами высших порядков и асинхронными системами переходов и т.д.
В последнее десятилетие резко возрос интерес к разработке и исследованию параллельных систем, поведение которых в значительной
степени зависит от количественных временных характеристик, — параллельных систем реального времени. Поэтому в литературе были сделаны попытки ввести понятие времени в различные формальные модели. В результате появились такие модели, как временные автоматы, временные системы переходов, временные сети-процессы, временные структуры событий, временные частично-упорядоченные множества и т.д. За последние пять лет были хорошо изучены взаимосвязи между временными сетями Петри и временными автоматами. Однако известно не так много результатов по сравнительному анализу других временных параллельных моделей. Причем работы с использованием теоретико-категорных методов, на сколько нам известно, совсем отсутсвуют. Кроме того, следует отметить, что семантика «истинного параллелизма» моделей с реальным временем также недостаточна изучена в литературе.
В рамках диссертационной работы предпринимается попытка заполнить указанные пробелы.
Все вышесказанное говорит об актуальности исследований, проводимых в рамках диссертационной работы.
Цель диссертации состоит в развитии и обобщении теоретико-ка-тегорных методов спецификации и верификации параллельных систем реального времени. Достижение цели связывается с решением следующих задач:
разработка и развитие формальных моделей параллельных систем реального времени;
построение и исследование абстрактной семантики временных параллельных моделей в терминах областей Скотта;
развитие и применение теоретико-категорных методов сравнительного анализа, классификации и унификации параллельных моделей с реальным временем.
Методы исследований. В рамках данной работы использовались методы и понятия теории категорий, теории множеств, теории графов, теории автоматов и теории частичных порядков. В качестве формальных моделей параллелизма применялись первичные, расслоенные и стабильные структуры событий, сети Петри и системы переходов с неза-
висимостью и их временные расширения.
Научная новизна. В результате выполненных исследований автором разработаны оригинальные методы решения задач построения семантики «истинного параллелизма» и установления взаимосвязей моделей параллельных систем реального времени. Следующие результаты, полученные в диссертации, полностью раскрывают научную новизну:
Разработаны временные расширения моделей с семантикой «истинного параллелизма» — временные первичные/расслоенные/стабильные структуры событий, а также временные системы переходов с независимостью.
Построена семантика помеченных областей Скотта для временных структур событий, временных систем переходов с независимостью и временных сетей Петри.
Определены и изучены категории введенных временных моделей, между которыми установлены строгие взаимосвязи в терминах существования коррефлексий.
Практическая ценность. Полученные результаты носят в основном теоретически характер. Тем не менее, они могут быть применены при разработке модулей автоматического построения семантических представлений, эквивалентных преобразований и верификации параллельных процессов, а также оптимизации параллельных программных систем.
Личный вклад автора. Все результаты, представленные в диссертации, получены автором лично. Постановки задач выполнены научным руководителем И.Б. Вирбицкайте.
Апробация работы. Основные идеи и конкретные результаты диссертационной работы обсуждались на следующих международных и отечественных научных конференциях и семинарах:
XLI Международная научная студентческая конференция «Студент и научно-технический прогресс» (Россия, Новосибирск, 2003);
Международная научно-практическая конференция по прорам-мированию УкрПРОГ'2004 (Украина, Киев, 2004);
International Conference on Parallel Computing Technologies
PaCT'2005 (Krasnoyarsk, Russia, 2005);
International Andrei Ershov Memorial Conference on Perspectives of System Informatics on (Novosibirsk, Russia, 2006);
15th International Workshop «Concurrency, Specification and Programming» (Vandlidz, Germany, 2006);
IX всероссийская конференция молодых ученых по математическому моделированию и информационным технологиям (Россия, Кемерово, 2008);
17th International Workshop «Concurrency, Specification and Programming» (Gross Vaeter See, Germany, 2008).
Кроме того, доклады по теме работы были сделаны на ряде семинаров Института систем информатики СО РАН (г. Новосибирск) и кафедр Новосибирского государственного университета.
Публикации. По теме диссертации опубликовано 9 научных работ, в том числе 1 — в изданиях, рекоммендуемых ВАК, 1 — в научном журнале, 6 — в трудах международных и отечественных конференций и семинаров.
Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения и списка литературы.
