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

• Автор: Коротиков, Сергей Викторович
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2008
• Место защиты: Новосибирск
• Количество страниц: 216 с. : ил.

СОДЕРЖАНИЕ

ВВЕДЕНИЕ
1. МЕТОДОЛОГИЧЕСКИЕ И ТЕХНОЛОГИЧЕСКИЕ ОСОБЕННОСТИ РАЗРАБОТКИ МНОГОПОТОЧНОГО ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ: ЦЕНТРЫ ДИСТАНЦИОННОГО УПРАВЛЕНИЯ И КОНТРОЛЯ
1.1 Архитектура и особенности функционирования многопоточного программного обеспечения: центры дистанционного управления и контроля
1.2. Анализ подходов к разработке программного обеспечения
1.3. Методы обеспечения правильности моделей
1.4. Анализ возможностей применеггия сетей Петри на технологическом цикле разработки программного обеспечения
1.5. Постановка задачи диссертационного исследования
2. ПРИМЕНЕНИЕ КЛАССИЧЕСКИХ И РАСКРАШЕННЫХ СЕТЕЙ ПЕТРИ В МОДЕЛИРОВАНИИ И АНАЛИЗЕ МНОГОПОТОЧНОГО ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ НА ПРИМЕРЕ ЦЕНТРОВ ДИСТАНЦИОННОГО УПРАВЛЕНИЯ И КОНТРОЛЯ
2.1. Применение классических сетей Петри для моделирования и анализа функционирования многопоточного программного обеспечения
2.2. Применение раскрашенных сетей Петри для моделирования и анализа функционирования многопоточного программного обеспечения

2.3. Анализ свойств раскрашенной иерархической сети Петри
при моделировании функционирования реальных систем
2.4. Применение компьютерных инструментов для моделирования и анализа раскрашенных иерархических сетей Петри
2.5. Выводы
3. ПРИМЕНЕНИЕ РАСКРАШ ЕННЫХ ИЕРАРХИЧЕСКИХ СЕТЕЙ ПЕТРИ НА ЭТАПЕ АНАЛИЗА
3.1. Методика создания и аттестации ЦМЬ-диаграмм этапа анализа
3.2. Шаблон ЦМЬ-диаграмм на этапе анализа
3.3. Преобразование набора ЦМЬ-диаграмм этапа анализа в раскрашенную иерархическую сеть Петри
3.4. Исследование модели и анализ результатов
3.5. Выводы
4. ПРИМЕНЕНИЕ РАСКРАШЕННЫХ ИЕРАРХИЧЕСКИХ СЕТЕЙ ПЕТРИ НА ЭТАПЕ ПРОЕКТИРОВАНИЯ
4.1. Методика разработки и проверки моделей
4.2. Шаблон ЦМЬ-диаграмм проекта службы управления и контроля
4.3. Преобразование набора иМЬ-диаграмм проекта в раскрашенную иерархическую сеть Петри
4.4. Моделирование и анализ
4.5. Выводы
5. ПРИМЕРЫ ИСПОЛЬЗОВАНИЯ СЕТЕЙ ПЕТРИ В РАЗРАБОТКЕ ЦЕНТРОВ ДИСТАНЦИОННОГО УПРАВЛЕНИЯ И КОНТРОЛЯ

5.1. Центр дистанционного управления и контроля таксофонов
5.2. Диспетчерский центр блоков релейной защиты
5.2.1. Применение методики создания и аттестации модели центра дистанционного управления и контроля на этапе анализа
5.2.2. Применение методики создания и аттестации модели проекта центра дистанционного управления и контроля
5.3. Выводы
ЗАКЛЮЧЕНИЕ
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ
ПРИЛОЖЕНИЯ
П. 1. Основные определения и свойства раскрашенных иерархических
сетей Петри
П.2. Рекомендации по повышению эффективности моделирования и
анализа в пакете CPN Tools
П.З. Модели диспетчерского центра блоков релейной защиты
П.4. Акты о внедрении результатов диссертационного исследования
П4.1. Диспетчерский центр блоков релейной защиты
П4.2. Центр дистанционного контроля и управления таксофонами
П4.3. Справка о внедрении результатов диссертационной работы в процесс обучения студентов НГТУ

Для преодоления разрыва между процессом разработки принятым в индустрии ПО и применением формальных методов необходимы методики, позволяющие легко использовать формальные модели и методы, реализованные в удобных для использования пакетах моделирования и которые будут органично вписываться в принятые в индустрии ПО подходы и методы разработки.
Формальные методы [1-5, 9-17, 19-23, 26-31, 33-43, 49-54, 58, 71, 74, 76, 79, 99, 100, 103, 104, 107-109, 112-116] позволяют систематически строить и анализировать формальные модели, отражающие различные аспекты или составные части создаваемой системы, и в дальнейшем трансформировать их в программы либо подбирать по ним готовые компоненты. Благодаря математическому аппарату, основанному на алгебре, логике и дискретной математике, правильность построения моделей и программ во многих случаях удается установить путем строгого доказательства, а хорошо подготовленные модели сами становятся интеллектуальной продукцией, предназначенной для многократного использования разработчиками. Особый интерес при разработке систем представляют шаблоны и легко модифицируемые шаблонные модели [23]. Проанализируем формальные методы, позволяющие проводить проверку UML моделей.
Описание основных концепций ООП средствами языка первого порядка обогащает язык UML до исчисления, позволяющего проводить доказательство правильности диаграмм. Обширная система аксиом и правил F-логики (Frame logic) [42], отражающих основные процедуры построения иерархии классов, превращает её в исчисление, обладающее свойствами непротиворечивости и полноты. Средствами этого исчисления можно верифицировать диаграммы классов.
Для анализа диаграмм UML можно привлекать методы теории графов, что позволяет строить различные формальные методики объектно-ориентированного проектирования. Например, исчисление путей в параметризованных множествах графов, представляющих словари диаграмм классов, лежит в основе метода Деметра [50], применяющегося для проектирования едино-