Методы анализа корректности параллельного и распределенного программного обеспечения на основе PS-сетей тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат технических наук Сарайкин, Андрей Витальевич

• Сарайкин, Андрей Витальевич
• кандидат технических наук
• 2000

Оглавление диссертации кандидат технических наук Сарайкин, Андрей Витальевич

ВВЕДЕНИЕ.

ГЛАВА 1 ПРОБЛЕМЫ ОБЕСПЕЧЕНИЯ КОРРЕКТНОСТИ ПРВ.

1.1 Основные понятия, характеризующие ПРВ.

1.2 Проблемы корректности ПРВ.

1.3 Требования к формальным моделям параллелизма.

1.4 Классификация и анализ формальных моделей параллелизма.

1.4.1 Структурные модели. Сети Петри и их расширения.

1.4.2 Семантические модели.

1.4.3 Логические модели.

1.5 Цель и задачи исследования.

Введение диссертации (часть автореферата) на тему «Методы анализа корректности параллельного и распределенного программного обеспечения на основе PS-сетей»

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

Чаще всего актуальная проблема обоснования надежности ПРПО сводится к проблеме обоснования его корректности. Решение последней основывается на использовании формальных моделей параллелизма (ФМП), позволяющих анализировать поведенческие свойства ПРПО [72, 73, 92].

В настоящее время предложено и исследовано большое количество ФМП ориентированных на решение различных задач, связанных с ПРВ и отличающихся, главным образом, степенью детализации моделируемых процессов и явлений. Наиболее развитыми ФМП являются сети Петри и их расширения. Важные результаты по этим ФМП обобщены в работах Питерсона Дж., Котова В.Е. и ряда других исследователей. Однако анализ показывает [85, 89, 90], что среди предложенных ФМП нет таких, которые бы в комплексе предоставляли следующие возможности:

• учет таких особенностей функционирования ПРВС, как наличие временных характеристик, конфликтов, разделяемых ресурсов и одновременного развития событий;

• наличие описательных средств, максимально удобных для практического применения при проектировании ПРПО;

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

В качестве наиболее приемлемого в этом смысле ФМП в [83, 86] предлагается и развивается аппарат Р8-сетей.

Актуальность данной темы определяется необходимостью создания новых и совершенствования предложенных ранее методов анализа ПРПО, описываемых на основе Р8-сетей.

Цель работы и задачи исследования. Целью диссертационной работы является создание математического и программного обеспечения для анализа корректности ПРПО на основе аппарата Р8-сетей. Для достижения этой цели в работе решаются следующие задачи:

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

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

3. Создание программных средств, реализующих предложенные методы и алгоритмы.

4. Исследование эффективности предложенных методов, алгоритмов и созданных программных средств, для чего следует решить ряд задач анализа корректности проектируемого ПРПО.

Апробация работы. Основные результаты работы докладывались и обсуждались на Международной конференции «Фундаментальные и прикладные проблемы охраны окружающей среды» (г. Томск, 1995 г.), на Международной конференции «Всесибирские чтения по математике и механике» (г. Томск, 1997 г.), на I Международном симпозиуме по науке и технологии КоКш'97 (г. Ульсан, Южная Корея, 1997 г.), на II Международном симпозиуме по науке и технологии КоЯш'98 (г. Томск, 1998 г.), на VI Международном семинаре 7

Распределенная обработка информации» РОИ'98 (г. Новосибирск, 1998 г.), на III сибирском конгрессе по прикладной и индустриальной математике ИНПРИМ'98 (г. Новосибирск, 1998 г.), на IV Международном симпозиуме по науке и технологии КоЯш^ООО (г. Ульсан, Южная Корея, 2000 г.).

По результатам исследований опубликовано 14 работ, в том числе 9 статей.

Личный вклад:

1. Постановки ряда рассмотренных в диссертации задач выполнены совместно с Н.Г. Марковым и Е.А. Мирошниченко, при этом математические формулировки задач исследований осуществлены автором.

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

3. Постановка задачи исследования корректности способов организации распределенной обработки информации в ГИС-сервере социально-экономической сферы субъекта федерации осуществлена совместно с Н.Г. Марковым и П.М. Острасть, разработка моделей ГИС-сервера проведена совместно с Е.А. Мирошниченко. Результаты исследования получены автором.

4. Постановка задачи определения верхних границ времени выполнения операций над данными пользователями «Регионального банка геологической информации по геологии нефти и газа и недропользованию» осуществлена В.В. Уваровым. Разработка моделей, описывающих функционирование регионального банка, а также их исследования проведены автором.

Коротко изложим основное содержание работы.

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

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

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

Рассматривается общая классификация ФМП. Для наиболее известных представителей каждого класса проводится комплексный анализ их описательных и аналитических возможностей с точки зрения удовлетворения выработанным требованиям.

Обосновывается выбор РБ-сетей как наиболее удобной ФМП для описания и анализа ПРПО на этапе его проектирования.

Формулируются цель и основные задачи, решаемые в диссертационной работе.

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

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

Для реализации предложенных методов и алгоритмов анализа поведенче9 ских свойств РБ-сети формулируются матричные определения РБ-сетей, их маркировки и правил функционирования.

Для расширения возможностей анализа Р8-сетей вводится понятие ее базового подкласса — ВРБ-сетей, равномощного Р8-сетям, для которого предлагаются разработанные теоретико-множественное и матричное представления.

Подробно рассматриваются и описываются матричные уравнения над ВРБ-сетями и типы ее структурной определенности. Предлагается теория асинхронной интерпретации ВРБ-сети, в основе которой лежит теорема о решении уравнения СА-перехода, построенного для линейно и полулинейно определенной ВР8-сети. В рамках предложенной теории на основе введенных понятий БУЯ- и БО-инвариантов, предлагается метод анализа поведенческих свойств ВР8-сетей.

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

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

Для решения задачи преобразования ВР8-сети к ВР8-сети полулинейно определенного вида предлагаются алгоритмы БрИШреобразований.

Для более эффективного решения задачи анализа ПРПО, а также для ком-пактификации описывающих его моделей, предлагается иерархический подход к спецификации ПРПО и обоснованию его корректности, основанный на введенном понятии метадуги и являющийся развитием предложенного в теории Р8-сетей [89] способа интеграции подсетей.

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

10

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

Для анализа ПРПО на основе PS-сетей в рамках инструментальной системы моделирования «Parallax» созданы программные средства, предоставляющие пользователю следующие основные возможности: обнаружение в модели локальных тупиков; осуществление преобразований PS-сети к BPS-сети; построение дерева покрытий (достижимости) для PS- и BPS-сети; осуществление преобразований BPS-сети к BPS-сети полулинейно определенного вида; интерпретацию вариантов поведения приведенной BPS-сети; построение SVR- и SD-инвариантов.

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

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

Рассмотрена задача исследования корректности проектируемых способов организации распределенной обработки информации в «ГИС-сервере социально-экономической сферы субъекта федерации», разработанного по заказу Государственного научно-исследовательского института информационных технологий и телекоммуникаций «Информика» г. Москва. ГИС-сервер предназначен для организации удаленного доступа пользователей к функциям геоинформационной системы средствами Web-технологии и создавался в рамках разработки распределенной геоинформационной системы. Разработанные модели и результаты их анализа использованы при проектировании ПО ГИС-сервера. Так в частности, при анализе моделей PS-сетей на основе предложенных методов и алгоритмов были обнаружены ошибки в проектных решениях и предложены способы их устранения.

11

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

Научную новизну полученных в работе результатов определяют.

• формальные определения поведенческих свойств Р Б-сетей и методы обнаружения этих свойств, предназначенные для обоснования корректности проектируемого ПРПО;

• матричное представление аппарата Р Б-сетей, а также теоретико-множественное и матричное представления базового подкласса аппарата РБ-сетей — ВРБ-сетей, предназначенных для формального анализа поведенческих свойств описываемого на их основе ПРПО;

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

• теория асинхронной интерпретации ВРБ-сетей, опирающаяся на ряд теорем, доказанных автором, и позволяющая на основе решения уравнения СА-перехода расширить возможности анализа ВРБ-сети в части применения метода инвариантов;

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

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

Практическая ценность и реализация результатов работы. Практически значимыми являются созданные модели, методы, алгоритмы и программные средства для анализа проектируемого ПРПО на предмет его корректности. Программные средства функционируют на ПЭВМ типа IBM PC в операционной среде Windows 95/NT. Объем разработанного на языке С++ ПО составляет более 6500 строк программного кода.

Предложенные модели, методы и алгоритмы, а также разработанные программные средства анализа ПРПО были внедрены в Государственном научно-исследовательском институте информационных технологий и телекоммуникаций «Информика» г. Москва при проектировании и исследовании корректности способов организации распределенной обработки информации в проекте «ГИС-сервер социально-экономической сферы субъекта федерации», разработанного для использования в сети Internet. Эти же методы, алгоритмы и программные средства внедрены при исследовании верхних границ времени выполнения операций над данными пользователями «Регионального банка геологической информации по геологии нефти и газа и недропользованию» в многопользовательском режиме, разработанного в Западно-Сибирском геологическом научно-аналитическом центре г. Тюмень. Созданные программные средства анализа ПРПО также были внедрены в учебный процесс на кафедре Автоматизации проектирования Томского политехнического университета в составе инструментальной системы моделирования параллельных процессов «Parallax» при выполнении цикла лабораторных работ по курсу «Современные архитектуры вычислительных машин, комплексов, систем и сетей» и подготовке магистров. Результаты внедрений подтверждаются соответствующими актами.

13

Основные положения, выносимые на защиту:

1. Предложенные методы и алгоритмы анализа ПРПО позволяют исследовать его корректность еще на этапе проектирования.

2. Теория асинхронной интерпретации ВР8-сети существенно расширяет возможности анализа поведенческих свойств описываемого на их основе ПРПО.

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

4. Разработанные теоретические положения, методы, алгоритмы и программные средства позволяют проектировать надежное и эффективное ПРПО.

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

14

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Сарайкин, Андрей Витальевич

4.5 Основные выводы по главе

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

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

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

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

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

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

149

ЗАКЛЮЧЕНИЕ

Диссертационная работа посвящена созданию математического и программного обеспечения для анализа корректности ПРПО на основе аппарата PS-сетей. Получены следующие основные научные и практические результаты:

1. Сформулированы формальные определения, характеризующие поведенческие свойства PS-сетей при исследовании корректности описываемого на их основе ПРПО.

2. Разработаны метод анализа поведенческих свойств PS-сетей на основе модификации алгоритма построения дерева покрытий и метод обнаружения локальных тупиков в PS-сети, основанный на поиске ЯР-инвариантов

3. Разработаны теоретико-множественное и матричное представления базового подкласса PS-сети — BPS-сети. Создана теория асинхронной интерпретации BPS-сетей, опирающаяся на ряд доказанных автором теорем и направленная на расширение возможностей анализа ее поведенческих свойств в части использования метода инвариантов.

4. Разработан метод анализа поведенческих свойств BPS-сети, базирующийся на решении уравнения синхронно-асинхронного перехода и понятиях SVR- и SD-инвариантов, введенных в рамках предложенной теории асинхронной интерпретации BPS-сети.

5. Разработан ряд алгоритмов преобразований над PS- и BPS-сетями, позволяющих осуществлять приведение произвольной PS-сети к BPS-сети полулинейно определенного вида.

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

150 уточнение временных характеристик объектов модели при интеграции в нее разверток метадуг.

7. Созданы программные средства, реализующие предложенные методы и алгоритмы анализа корректности ПРПО, описываемого на основе PS-сетей. Разработанное ПО функционирует на IBM PC-совместимых ПЭВМ под управлением ОС Windows 95/NT и состоит из более чем 6500 строк программного кода на языке С++.

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

9. Разработанные методы, алгоритмы, программные средства, модели и результаты исследований моделей внедрены в Государственном научно-исследовательском институте информационных технологий и телекоммуникаций «Информика» г. Москва и в Западно-Сибирском геологическом научно-аналитическом центре г. Тюмень. Программные средства анализа ПРПО также внедрены в учебный процесс в Томском политехническом университете.

Список литературы диссертационного исследования кандидат технических наук Сарайкин, Андрей Витальевич, 2000 год

1. Agerwala Т., Flynn М. A Complete Model for Representing the Coordination of Asynchronous Processes. — In: Hopkins Computer Research. Report 32. Baltimore, 1974.

2. Alur R, Courcoubetis C., Dill D. Model-checking for Real-time systems. Proc. 5*1 IEEE LICS, 1990, p. 214-225. AlurR., DillD. The Theory of Timed Automata. Lect. Notes Comput. Sci. — 1991. — Vol. 600. — p. 45-73.

3. Boudol G., Castellani I. On the Semantics of Concurrency: Partial Orders and Transition Systems // Lect. Notes Comput. Sci. — 1987. — Vol. 249.—p. 123-137.

4. Boyer R.S., Moore J.S. Computation Logic Handbook. Academic Press, Volume 23 of Perspectives in Computing, 1988. Brams G.W. Reseaux de Petri: Theorie et Pratique. V. 1-2. Paris: Mas-son, 1983.

5. Clarke E.M., Emerson E.A., Sistla A.P. Automatic Verification of Finite-State Systems Using Temporal Logic Specifications. ACM TOPLAS 8(2), 1986, p. 244-263.

6. Courtois P.J., Heymans F., Parnas D.L. Concurrent Control with Readers and Writers. — Communs ACM, 1971, vol. 14, № 10, p. 667668.

7. Czaja L. A Calculus of Nets // Кибернетика и системный анализ. — 1993, —№2, —с.40-50.

8. GenrichH. J., Lantenbach К., ThiagarajanP.S. Elements of General Net Theory // Lect. Notes Comput. Sei. — 1980. — Vol. 84. — p. 21163.

9. Ghezzi C. Concurrency in Programming Languages: a Survey // Parallel computing: 1985. — № 2. — p. 229-241.

10. Gilbert P., Chandler W.J. Interference Between Communicating Parallel Processes. — Communs ACM, 1972, vol. 15, № 6, p. 427-437.

11. Harel D. Biting the Silver Bullet // IEEE Computer. 1992. — Vol. 25. — № 1,—p. 514-520.

12. HenzingerT.A., Manna Z., PnueliA. Timed Transition Systems. Lect. Notes Comput. Sci. — 1991. -—Vol. 600. — p. 226-251. Holt R.C. Some Deadlock Properties of Computer Systems. — ACM Comput. Surv., 1972, vol. 4, № 3, p. 179-196.

13. Karp R., Miller R. Parallel Program Schemata, RC-2053, IBM T.J. Watson Research Center, Yorktown Heights, New York, 1968, pp. 54. Katoen J.P. Qualitative and Qualitative Extensions of Event Structures. PhD Thesis, Twente University, 1996.

14. Markov N., Ostrast P. Distributed Web-based GIS, Proc. 2nd AGILE Conference on Geographic Information Science, Rome, Italy, April 1517, 1999, p. 53.

15. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Analysis of Parallel Computation Correctness With the Use of PS-nets // In: Abstracts of the 2nd Korea-Russia Int. Symp. on Sei. and Tech. — Tomsk, TPU, 1998.—p. 253.

16. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Method and Tools for Parallel and Distributed Software Creation // In: Proceedings of the 1st Korea-Russia Int. Symp. on Sei. and Tech. — Ulsan, Ulsan University, 1997. — p. 389-394.

17. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Method and Tools for Parallel and Distributed Software Creation // In: Abstracts of the 1st Korea-Russia Int. Symp. on Sei. and Tech. — Ulsan, Ulsan University, 1997,—p. 205.

18. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Technology of Design of Distributed Applications with the Use of PS-nets // Join Bulletin of NCC and IIS, Series Computer Science, Novosibirsk. — №12, 1999, —p. 32-36.

19. Milner R. A Calculus of Communicating Systems // Lect. Notes Comput. Sei. —1980.—Vol. 92.

20. Nielsen M., Plotkin G., Winskel G. Petri Nets, Event Structures and Domains // Theoretical Computer Science. — 1981. — Vol. 13. — p. 85-108.

21. Nielsen M., Thiagarajan P.S. Degrees of Non-determinizm and Concurrency: A Petri Net View // Lect. Notes Comput. Sei. — 1984. — Vol. 181. —p. 89-117.

22. Noe J.D., Nutt G.J. Macro E-nets for Representation of Parallel Systems // IEEE Trans. Computers, Aug. — 1973. — Vol. C-22. — p. 718727.

23. Ostroff J.S. Temporal Logic of Real-time Systems. Research Studies Press, 1990.

24. Park D. Concurrency and Automata on Infinite Sequences // Lect. Notes Comput. Sei. — 1981. — Vol. 104. — p. 167-183. Patil S. Coordination of Asynchronous Events. — Massachusetts, June 1970, —234 p.

25. Petri C.A. Kommunikation mit Automaten. — Technische Hochschule Darmstadt, 1962.

26. Plotkin G. An Operational Semantics for CSP // Formal description ofprogramming concepts. II. N.-H. Press, 1983. P. 199-223.

27. Pomello L. Some Equivalence Notions for Concurrent Systems. Anoverview//Lect. Notes Comput. Sci. — 1986. — Vol. 222. — p. 381—400.

28. Schneider S., Davies J., Jackson D.M., Reed G.M., Reed J.M., Roscoe A.W. Timed CSP: Theory and Practice. Lect. Notes Comput. Sci. — 1991. — Vol. 600. — p.640-675.

29. Sinachopoulos A. Partial Order Logics for Elementary Net Systems: State- and Event Approches // Lect. Notes Comput. Sci. — 1990. — Vol. 458.

30. Valk R. On the Computational Power of Extended Petri Nets // Lect. Notes Comput. Sci. — Berlin: Springer-Verlag, 1978. — Vol. 64. — p. 526-535.

31. Valk R. Self-modifying Nets, a Natural Extension of Petri Nets. — In: Lect. Notes Comput. Sci. — Berlin: Springer-Verlag, 1978. — Vol. 62. — p. 464-476.

32. Van der Aalst W.M.P. Interval Timed Coloured Petri Nets and Their Analysis // Lect. Notes Comput. Sci. — 1993. — Vol. 691. — p. 453472.

33. Van Glabbeek R.J., Vaandrager F. Petri Net Models for Algebraic Theories of Concurrency // Lect. Notes Comput. Sci. — 1987. — Vol. 259.—p. 224-242.

34. Vogler W. Bisimulation and Action Refinement // Lect. Notes Comput. Sci. — 1991. — Vol. 480. — p. 309-321.

35. Wang F. Timing Behavior Analysis for Real-Time Systems. Proc. 10th IEEE LICN, 1995, p. 112-122.

36. Алгоритмы, математическое обеспечение и архитектура многопроцессорных вычислительных систем / Под ред. А.П. Ершова. — М.: Наука, 1982. — 336 с.

37. Ачасова С.М., Бандман O.JI. Корректность параллельных вычислительных процессов. — Новосибирск: Наука. Сиб. отд-ние, 1990. 253 с.

38. Бандман О.Л. Поведенческие свойства сетей Петри (обзор французских работ) // Известия АН СССР, Техническая кибернетика, 1987, № 5, с. 134-150.

39. Барский А.Б. Параллельные процессы в вычислительных системах. Планирование и организация. — М.: Радио и связь, 1990. — 256 с.

40. Вотинцева A.B. Методы спецификации и анализа параллельных процессов, представленных структурами событий: автореферат диссертации на соискание ученой степени к.ф-м.н. Новосибирск. — 1997, — 16 с.

41. ГИС-сервер Социально-экономической сферы Томской области. — http : Wee. cctpu. edu. ru\gis\

42. Йодан Э. Структурное проектирование и конструирование программ: Пер. с англ./Под ред. Л.Н.Королева. — М.: Мир, 1979. 416 с.

43. Котов В.Е. Сети Петри. —М.: Наука, 1984. — 158 с.

44. Липаев В.В. Качество программного обеспечения. — М.: Финансыи статистика, 1983. — 264 с.

45. Липаев В.В. Проектирование программных средств. — М.: Высш. шк., 1990,—303 с.

46. Майерс Г. Искусство тестирования программ: Пер. с англ. — М.: Финансы и статистика, 1982. 178 с.

47. Мирошниченко Е.А. Четырехэтапная технология создания параллельного программного обеспечения // Кибернетика и ВУЗ. — 1999. — Вып. 29. — с. 126-136.

48. Покозий Е.А. Методы спецификации и верификации параллельных моделей с непрерывным временем: диссертация на соискание ученой степени кандидата физико-математических наук. Новосибирск, ИСИ СО РАН. — 1999. — 76 с.

49. Сарайкин A.B. Сравнительный анализ моделирующей мощности PS-сетей и классических сетей Петри // Кибернетика и ВУЗ. — 1999. — Вып. 29. — с. 83-94.

50. Смелянский P.JI. Вестник Моск. Ун-та. Сер. 15. Вычисл. матем. и Кибернетика. 1990. № 3. с.3-18.

51. Тарасюк И.В. Алгебра AFLTV исчисление помеченных недетерминированных параллельных процессов// Проблемы спецификации и верификации параллельных систем. — Новосибирск. — 1995, —с. 22-49.

52. Уваров В.В., Хафизов Ф.З., Шаталов Г.Г. Опыт создания регионального банка цифровой геологической информации: Материалы Межрегиональной конференции. — Томск: ГалаПрес, 2000. — Том 2.— с. 428-430.

53. Устименко А.П. Отображение временных причинно-следственныхструктур во временные сети Петри // Кибернетика и системныйанализ. Киев, 1997, № 2, с. 44-54.

54. Фейс Р. Модальная логика. — М.: Наука, 1974. — 520 с.

55. Хоар Ч. Взаимодействующие последовательные процессы: Пер. сангл. — М.: Мир, 1989. — 264 е., ил.

56. Шоу А. Логическое проектирование операционных систем: Пер. с англ.—М.:Мир, 1981. — 360 с. ил.161