Актуальность темы
.
В настоящее время усилился интерес к динамическим моделям систем, состоящих из большого числа взаимодействующих компонентов. Для решения задач моделирования таких систем требуется разработка методов моделирования, специально ориентированных на автоматизацию процессов синтеза и анализа моделей с использованием вычислительных мощностей современных персональных компьютеров. Создание и развитие автоматизированных методов моделирования является актуальной темой научных исследований.
Одним из перспективных направлений развития автоматизированных методов, является разработка методов моделирования с использованием дискретных потоков. Основы методов моделирования с использованием дискретных потоков заложены в 2001;2002 годах Ф. Арбабом, М. Бройем, Я. Руттеном, К.Столоном.
В методе Броя и Столена входы и выходы каждого компонента системы, называемого объектом, моделировались при помощи потоков. Внутренние состояния объектов не рассматривались. Синхронность потоков не использовалась. Семантика объектов задавалась при помощи функций, преобразующих потоки на входах в потоки на выходах.
В методе Руттена и Арбаба предложены два варианта семантики: ко-алгебраическая и на основе конечных автоматов. Как и в работах Броя и Столена, потоки использованы для моделирования входов и выходов объекта. В коалгебраической семантике внутренние состояния объектов не рассматривались. В семантике на основе конечных автоматов внутренние состояния определены внутренними состояниями соответствующего конечного автомата. Унификация способа моделирования входов, выходов и внутренних состояний не проведена. Синхронность потоков не использована.
Для развития методов моделирования с использованием дискретных потоков важными задачами являются: разработка эффективных унифицированных способов представления входных, выходных и внутренних переменных объектов и их систем, модификация этих методов с целью создания алгоритма анализа всех вариантов поведения моделей.
Цель диссертационной работы.
Разработка метода синхронных потоков для дискретного моделирования динамических систем, создание алгоритмов, автоматизирующих синтез моделей систем, построение и анализ вариантов их поведений.
Научная новизна.
В диссертации.
1. Введено понятие синхронных потоков, доказаны теоремы об их основных свойствах, которые легли в основу метода синхронных потоков.
2. Разработан метод синхронных потоков, предназначенный для дискретного, автоматизированного моделирования вариантов поведения объектов и их систем.
Разработано унифицированное представление входов, выходов и внутренних переменных объектов через наборы синхронных потоков.
3. Разработаны модификации линейной темпоральной (временной) логики для работы с бесконечными потоками и их фрагментами. Темпоральная логика использована для строгой математической записи временных свойств возможных поведений объектов и их систем.
4. В методе синхронных потоков разработаны.
4.1. Алгоритм синтеза математической модели системы по заданной структуре и по моделям составляющих систему объектов.
4.2. Алгоритм построения фрагментов вариантов поведений объекта или системы объектов и алгоритм анализа выполнимости ими временных (темпоральных) свойств.
5. Методом синхронных потоков разработаны дискретные модели: простого производственного объекта, простого складского объекта, складского объекта с учетом динамики его основных фондов, внешнего поставщика фондов, внешнего заказчика готовой продукции.
Используя разработанный алгоритм синтеза математических моделей систем, получена модель замкнутой системы производственного объекта с поставщиками, заказчиком и управляющим объектом.
Разработанная модель решает задачу автоматического построения и анализа вариантов развития системы, позволяет менеджеру проанализировать все варианты развития и выбрать один из них.
Методы исследования.
Методы исследования базируются на методах алгоритмизации, дискретного моделирования процессов, теории универсальных коалгебр, темпоральных логик, логике первого порядка.
Теоретическая и практическая значимость.
Разработанный метод синхронных потоков, алгоритмы, основные идеи и утверждения, предложенные в диссертации, развивают эффективное направление в математическом моделировании через дискретные потоки и открывают дополнительные возможности исследования широкого класса динамических моделей с использованием вычислительных мощностей современных компьютеров.
Метод синхронных потоков применен для синтеза математических моделей систем производственных объектов, построения фрагментов всех вариантов поведений таких систем и анализа выполнимости ими временных свойств.
Апробация работы.
Результаты диссертации докладывались и обсуждались на следующих конференциях: Workshop on Specification and Verification of Component-Based Systems (Лиссабон, 2005), CONCUR (Лондон 2004), International Workshop on Coalgebraic Methods in Computer Science (Барселона 2004), ETAPS (Барселона 2004), Всероссийская научно-практическая конференция «Инновации в науке, технике, образовании и социальной сфере» (Казань 2003), Международная научная конференция «Компьютерное моделирование и информационные технологии в науке, инженерии и образовании» (Пенза 2003), на школах-семинарах International Marktoberdorf Summer School (Мюнхен, 2004 и 2005), на семинарах Института теоретической информатики Технического университета Дрездена (Дрезден, 2003;2005), кафедры Управления, маркетинга и предпринимательства Казанского государственного технического университета им. А. Н. Туполева (Казань, 2003;2005).
Используемые формализмы.
В этой секции определены понятия, использованные при задании математической семантики метода синхронных потоков. Семантика метода синхронных потоков основана на понятиях финальных коалгебр бесконечных потоков элементов (из заранее определенного множества) и их подкоалгебр.
Далее приведен необходимый минимум определений. Теория универсальных коалгебр подробно рассмотрена в работах [80], [90] а также [62, 79, 75, 76, 77, 86, 56, 60, 61].
Теория универсальных коалгебр является сравнительно молодым направлением в теоретической информатике, поэтому многие определения теории коалгебр базируются на теории категорий или на принципе дуальности и на дуальных определениях из теории универсальных (абстрактных, высших) алгебр. Теория универсальных алгебр подробно рассмотрена в работах [31, 7, 46, 23, 8, 21, 9, 24, 28, 20, 53]. Теория категорий изложена в работах [96, 48, 5, 47, 64, 95, 73, 63, 83].
Теория категорий.
Теория категорий — это раздел математики, изучающий свойства отношений между математическими объектами, независящие от внутренней структуры самих объектов.
Определение 0.0.1. Категория С состоит из класса объектов objc и класса arre стрелок или морфизмов таких что:
• для каждого морфизма / G arre определена его область определения и область значений. Пусть областью определения морфизма / является объект A? objc, а областью значений — объект В G objc, тогда морфизм / определен как:: А^В.
• для каждой пары морфизмов /: А —> В и д: В —> С определена их композиция:
9 о/: А-+С.
• для каждого объекта, А задан тооюдественный морфизм 1(1 а’а'. АА.
• выполняются нижеследующие законы ассоциативности и толс-дествеииости морфизмов.
Аксиома 0.0.2 (Закон тождественности). Тождественные морфизмы действуют тривиально. Пусть /: А —> В, тогда: о1йА = «/до/ = /.
Аксиома 0.0.3 (Закон ассоциативности). Операция композиции ассоциативна. Пусть f: АВ, д: В С и Н: С И тогда:
Л ° (3 ° /) = (Л°р)о/.
Стандартным способом описания утверждений теории категорий являются коммутативные диаграммы.
Определение 0.0.4. Коммутативная диаграмма — это ориентированный граф, в вершинах которого находятся объекты, а стрелками являются морфизмы, причём результат композиции стрелок не зависит от выбранного пути.
Приведенные выше аксиомы теории категорий записаны с помощью коммутативных диаграмм, изображенных на рис. 1. Слева изображена коммутативная диаграмма закона тождественности, справа — коммутативная диаграмма закона ассоциативности.
Рис. 1: Коммутативные диаграммы двух аксиом теории категорий: коммутативная диаграмма закона тождественности (слева) и коммутативная диаграмма закона ассоциативности (справа).
Определение 0.0.5. Морфизм /: А —> В называется изоморфизмом, если существует такой морфизм g: В —" А, что.
70/ = idа и f од = idB.
Определение 0.0.6. Два объекта, А и В, между которыми существует изоморфизм, называются изоморфными, А = В.
В частности, для любого объекта, А тождественный морфизм id^ является изоморфизмом, поэтому любой объект изоморфен сам себе.
Определение 0.0.7. Для категории С определена дуальная ей категория Сор, в которой:
• объекты совпадают с объектами исходной категории:
A G obj с°р если и только если A G obj с.
• морфизмы получены «обращением стрелок»: fop: В —> A G arr с°р если и только если f: Л —В G arr с.
Для любого утверждения теории категорий можно сформулировать дуальное утверждение с помощью обращения стрелок. Дуальное явление обозначается тем же термином, но с приставкой «ко-» .
Определение 0.0.8. Произведение объектов, А я В это объект Ах В с двумя морфизмами р: А х В —> А и P2: А х В —> В такой, что для Р1, «р2.
А ¦*-А х В-* В.
А-^А + В^-В у С С.
Рис. 2: Коммутативная диаграмма произведения объектов (слева) и коммутативная диаграмма суммы объектов (справа) любого объекта С с морфизмами /1: С —> А и /2: С -> В существует единственный (уникальный) морфизм {/ь/2): С Ах В такой, что:
Определение 0.0.9. Сумма, копроизведепие объектов, А я В это объект, А + В с двумя морфизмами ц: А, А + В и: В —> А +В такой, что для любого объекта С с морфизмами д1: А —> С и д2: В —> С существует единственный (уникальный) морфизм [(71, <72]: А + В —* С такой, что:
Определение произведения объектов 0.0.8 наглядно представлено в виде коммутативной диаграммы слева на рис. 2, а определение 0.0.9 суммы объектов — в виде коммутативной диаграммы справа на рис. 2.
Теорема 0.0.10. Если произведение и копроизведепие существуют, то они определяются однозначно с точностью до изоморфизма.
Определение 0.0.11. Универсальный или инициальный объект категории — это такой объект, из которого существует единственный морфизм в любой другой объект этой категории.
Теорема 0.0.12. Если универсальный объект в категории существует, то он определяется с точностью до изоморфизма.
Дуальным образом определяется финальный или коуниверсальный объект.
Р1 ° (/ъ /2) = /1 и Р2°(/ь/2) = /2 дъд2]°ч = д и [01,02] о г2 = 92.
Определение 0.0.13. Финальный, терминальный или коуниверсаль-ный объект категории — это такой объект, в который из любого другого объекта категории существует единственный морфизм.
Теорема 0.0.14. Если финальный объект в категории существует, то он определяется с точностью до изоморфизма.
Введем понятие функтора, которое потребуется для описания коалгебр.
Определение 0.0.15. Функтор — это отображение одной категории в другую, сохраняющее структуру. Функтор F: С —" В ставит в соответствие каждому объекту категории С объект категории В и каждому морфизму /: А —> В категории С морфизм F (f): F (A) —> F{B) категории В так, что:
• сохранены тождественные морфизмы:
F (idA) = idF{A).
• сохранены композиции морфизмов:
F (g°f) = Hd) oF (f).
Определение 0.0.16. Категория Set функций и множеств — это категория, объектами в которой являются множества, морфизмами — тотальные функции.
В категории Set универсальный объект — это пустое множество 0, терминальным объект — любое множество, состоящее из одного элемента. Терминальный объект обозначен через 1 = {*}.
Алгебры.
Определение 0.0.17. Пусть F: Set —> Set функтор в категории Set функций и множеств. F-алгебра — это пара (Ма), состоящая из множества М и функции, а: F (M) —> М. Множество М названо несущим мнооюеством алгебры. f{M1)-^IF (M2) ai Q2.
Mx-f-^M2.
Рис. 3: Коммутативная диаграмма F-гомоморфизма между двумя F-алгебрами.
Определение 0.0.18. F-гомоморфизм между двумя F-алгебрами — это функция /: М —> М2, отображающая одну F-алгебру (Mi, ai) в другую-алгебру (М2, <22), такая что: о ax = а2 о F (f).
На рис. 3 представлена коммутативная диаграмма-гомоморфизма между двумя F-алгебрами.
Определение 0.0.19. Для функтора F: Set —> Set семейство F-алгебр вместе с F-гомоморфизмами между ними образуют категорию Alg (F) алгебр функтора F.
Определение 0.0.20. F-алгебра (/- т) является инициальной если из нее существует точно один гомоморфизм в любую F-алгебру.
Инициальные алгебры одного и того же функтора уникальны вплоть до изоморфизма.
Определение 0.0.21. Пусть задана F-алгебра (М-а). Непустое подмножество R С (М-а) называется F-подалгеброй (или F-субалгеброй), если пара (Яа) сама является F-алгеброй.
Коалгебры.
Определение 0.0.22. Пусть F: Set —> Set функтор в категории Set функций и множеств. F-коалгебра — это пара (Ма), состоящая из множества М и функции, а: М —> F (M). Множество М называется несущим мноэ/сеством коалгебры.
Мх-f—*M2.
Q 2 i F{1.
Рис. 4: Коммутативная диаграмма F-гомоморфизма между двумя F-коалгсбрами.
Определение 0.0.23. F-гомоморфизм между двумя F-коалгебрами — это функция /: Mi —> М2, отображающая одну F-коалгебру (Mi, ai) в другую Р-коалгебру (М2, «2), такая что:
2 о / = F (/) о ai.
На рис. 4 представлена коммутативная диаграмма F-гомоморфизма между двумя F-коалгебрами.
Определение 0.0.24. Для функтора F: Set Set семейство F-коалгебр вместе с F-гомоморфизмами между ними образуют категорию Coalg (F) коалгебр функтора F.
В этой категории нас интересует прежде всего финальная коалгебра (в случае, если она существует).
Определение 0.0.25. F-коалгебра (Р- 7г) является финальной если из любой F-ко алгебры существует точно один гомоморфизм в (Р- 7г).
Финальные коалгебры одного и того же функтора уникальны вплоть до изоморфизма. Для многих функторов финальная коалгебра существует и известна, кроме того для многих функторов она строится каноническим путем [87].
Определение 0.0.26. Пусть задана F-коалгебра (Ма). Непустое подмножество R С (Ма) называется F-подкоалгеброй (или F-субкоалге-брой), если пара (R', a) сама является F-коалгеброй.
Основные результаты диссертационной работы.
В диссертационной работе получены следующие основные результаты:
1. Введено понятие синхронных потоков, доказаны теоремы об их основных свойствах, которые легли в основу метода синхронных потоков.
2. Разработан метод синхронных потоков, предназначенный для дискретного, автоматизированного моделирования вариантов поведения объектов и их систем. Разработано унифицированное представление входов, выходов и внутренних переменных объектов через наборы синхронных потоков.
3. Для метода синхронных потоков разработана композиционная ко-алгебраическая семантика, т. е. семантика, в которой объединение объектов в систему трактуется как новый объект. Композициональ-ность семантики значительно упрощает работу с ней и облегчает создание алгоритма синтеза моделей и алгоритмов проверки выполнимости моделями временных (темпоральных) свойств.
4. В методе синхронных потоков разработан алгоритм синтеза математической модели системы. По заданной структуре и по моделям составляющих систему объектов строится модель системы.
5. Разработаны модификации линейной темпоральной (временной) логики для работы с бесконечными потоками и их фрагментами.
Темпоральная логика использована для строгой математической записи временных свойств возможных поведений объектов и их систем.
6. В методе синхронных потоков разработаны алгоритмы построения фрагментов вариантов поведений объекта или системы объектов и анализа выполнимости ими временных свойств.
7. Методом синхронных потоков разработаны дискретные модели: простого производственного объекта, простого складского объекта, складского объекта с учетом динамики его основных фондов, внешнего поставщика фондов, внешнего заказчика готовой продукции.
Используя разработанный алгоритм синтеза математических моделей систем, получена модель замкнутой системы производственного объекта с поставщиками, заказчиком и управляющим объектом.
Разработанная модель решает задачу автоматического построения и анализа вариантов развития системы, позволяет менеджеру проанализировать все варианты развития и выбрать один из них.
