ВВЕДЕНИЕ 2
1. ПРОЕКТИРОВАНИЕ ФОРМАЛЬНОЙ МОДЕЛИ В СРЕДЕ SPIN 3
1.1. Обзор верификатора Spin 3
1.2. Обзор языка Promela 3
1.3. Описание построения модели в виде иерархических блоков
управления 4
1.4. Описание параметров, характеризующих систему 7
1.5. Описание специфичных характеристик системы 14
1.6. Промежуточный вывод 15
1.7. Описание модели в виде иерархических блоков управления 16
1.8 Проверка свойств системы 35
1.9 Задача планирования 38
1.10 Описание цели и ограничений 39
1.11 Описание экспериментов 40
2. ПРОЕКТИРОВАНИЕ ФОРМАЛЬНОЙ МОДЕЛИ В СРЕДЕ PDDL... 42
2.1. Обзор верификатора PDDL 42
2.2. Описание построения модели с помощью базовых действий 43
2.3 Описание экспериментов 44
3. СРАВНИТЕЛЬНЫЙ АНАЛИЗ ИСПОЛЬЗОВАНИЯ СРЕДСТВ SPIN И
PDDL ДЛЯ РЕШЕНИЯ ЗАДАЧ ПЛАНИРОВАНИЯ 42
ЗАКЛЮЧЕНИЕ 47
СПИСОК ИСПОЛЬЗОВАННОЙ ЛИТЕРАТУРЫ 48
ПРИЛОЖЕНИЕ
В настоящее время программно-целевые методы стали основными в управлении социальными объектами различной природы (университеты, регионы, отрасли и пр.). Центральным элементом этих методов является разработка программы развития соответствующего социального объекта на достаточно долгий период времени. Правильность программы означает, что она корректно решает ту задачу, для которой она была разработана. В теоретическом программировании в таком случае говорят, что программа соответствует своей спецификации, понимая под спецификацией описание решаемой задачи на некотором формализованном языке.
Главная цель работы состоит в том, чтобы найти траекторию устойчивого развития такого социально-экономического объекта как
институт, то есть выявить такую программу развития, при которой будут достигнуты поставленные цели и на протяжении которой объект будет устойчиво функционировать.
Задачи ставятся следующие: во-первых, построить формальную
(математическую) модель исследуемой системы, которая корректно отражает возможное поведение системы; во-вторых, осуществить поиск траектории устойчивого развития такого социально-экономического объекта как
институт.
Поставленные задачи, в ходе работы над данной выпускной квалификационной работе, можно считать полностью выполненными: поострена формальная (математическая) модель исследуемой системы, которая корректно отражает возможное поведение системы, осуществлен поиск траектории устойчивого развития такого социально-экономического объекта как институт.
В ходе работы была проделана аналитическая работа по изучению схем функционирования института, структур международных рейтингов университетов, систем мониторинга вузов и пр. Полученные знания помогли построить «правильную» модель исследуемой системы. Также по результатам поиска траектории устойчивого развития изучаемой системы выяснилось, что инструмент планирования SPIN наилучшим образом подходит для решения данной задачи, так как язык построения модели этого инструмента способен более корректно отразить поведение исследуемого объекта.
На данный момент многие крупные социально-экономические системы разрабатывают внутренние планы развития. В связи с этим возникает проблема, как определить, что построенный план является «правильным», то есть можем ли мы утверждать, что разработанная схема приведет нас к поставленным целям. Данная выпускная квалификационная работа решает эту проблему путем построения формальной модели системы и поиска траектории устойчивого развития разработанной системы путем решения проблемы планирования, используя инструменты планирования SPIN и PDDL.
