Инструментальная среда имитационного моделирования

3.2 Задача о философах с дедлоком

Постановка задачи

Имеется круглый стол, вокруг которого стоят стулья, на которых сидят философы. В центре стола находится тарелка с макаронами. Рядом с каждым философом лежит салфетка (между 2 соседними философами лежит одна салфетка), а на каждой салфетке лежит вилка. Философ может либо думать, либо есть макароны. Для того чтобы думать ему достаточно находится на стуле. Для того чтобы есть ему необходимо держать в каждой руке по вилке.

Цели моделирования и анализа

Данная задача интересна на предмет анализа свойства наличие «тупиковой ситуации».

Решение

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

Рисунок 15. Системная сеть задачи о философах с дедлоком

Рисунок 16. Автоматная сеть задачи о философах с дедлоком на примере третьего философа в некоторый момент времени

Загрузим модель в TRDA Tool - выполним 50 шагов - Нажмем кнопку «Результаты анализа» - Рис. 17



Рисунок 17. Загружена модель задачи о философах с дедлоком, возник дедлок на 12 шаге

Как видно из разметки системной сети, прошло только 12 шагов и 2 момента времени, а все философы взяли по левой вилке, и вариантов дальнейшего переходов нет. Это произошло из-за того, что ни один философ не может взять левую вилку, чтобы поесть. А положить вилку по модели из Приложения 3 философ может только, когда поест (см. Рисунок 16)

В протоколе «Результаты анализа» отмечено наличие «тупиковой ситуации» в данной модели.

3.3 Задача о спящем парикмахере

Классическая постановка задачи

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

Начальная разметка системной сети построенной TRDA модели имеет следующий вид

Рисунок 18. Визуализированная системная сеть в задаче о спящем парикмахере

Как видно есть три вершины системной сети:

Street - улица, по которой гуляют люди, как стриженные, так и нестриженные

Reception - приемная, где люди ожидают своей очереди к парикмахеру

Chair - место, где человек стрижется

Имеются следующие агенты и/или ресурсы:

На улице имеется 4 стриженных человека

В приемной парикмахерской находится менеджер и есть 4 свободных места

В кресле «спит» парикмахер

Текущая интерпретация данной задачи имеет следующее описание:

В вершине системной сети street находится некоторое количество стриженых людей, (сложных агентов). На улице люди через некоторое время по счетчику «x» (ограничение x>30) обрастают волосами, становятся нестрижеными. Обросшие люди могут быть доставлены в приемную парикмахерской, в случае наличие там свободных мест. Данную операцию выполняет менеджер парикмахерской. «Спящий» (находящийся в состоянии «спит») парикмахер берет человека из очереди парикмахерской на стул стрижки и начинает его стричь (переходит в состояние «работает»). После стрижки, которую выполняется парикмахер над человеком, парикмахер отправляет человека на улицу в состоянии new_shorn, то есть свежеподстриженный, а сам «засыпает» (переходит в состоянии «спит»). Человек сам меняет свое состояние с new_shorn на shorn, при этом обнуляется счетчик «x» у этого человека.

Иными словами, можно сказать, что счетчик «x» - контроль необходимости в стрижке.

Зададим в исходном файле (приложение 3) необходимость проверки свойства достижимости, а именно, что все люди в течение выполнения модели попадут на стул парикмахера и, соответственно, будут там стричься. Проверяемое свойство выглядит следующим образом:

marking(m1,like)

place(chair)

inst(m01,shorning)

inst(barber,work)

Задавая свойство достижимости m1, мы говорим, что хотим проверить не все вершины системной сети (для этого в определении разметки используется ключевое слово like), а лишь проверить агентов и их состояния в вершине системной сети chair. Так, мы хотим убедиться, что там есть парикмахер (агент barber) в состоянии «работающий» (work) и агент типа «Человек» (m01, в данном случае) в состоянии «стрижка» (shorning).

Аналогичным образом зададим разметки m2, m3, m4 для агентов m02, m03 и m04 соответственно.

Загрузив модели в TRDA Tool, проверим данное свойство, выставив галочку Достижимость, выполним некоторое количество шагов. Затем, нажав кнопку «Результаты», проверим достижимости заданной маркировки.



Рисунок 19. Достижимость для задачи о спящем парикмахере

Как видно, все требуемые разметки (m1, m2, m3, m4) были достигнуты, значит, модель составлена правильно.

Теперь посмотрим отображение хода выполнения модели на временной диаграмме (нажав кнопку Временная диаграмма - Рис. 20)

Рисунок 20. Временная диаграмма задачи о спящем парикмахере

Так же на примере данной модели просмотрим структурное и графическое представление текущего состояния автоматной сети на примере агента m02. Для этого выставим звездочку на этом агенте в структурном виде представления модели. Звездочка выставляется двойным кликом по агенту - Рис. 21.



Рисунок 21. Звездочка на агенте m02

Теперь выставим галочку Автоматная сеть и просмотрим структуру агента - рис. 22

Рисунок 22. Агент m02

Видно, что не все состояния связаны стрелочками. Это происходит из-за того, что в некоторые состояния агент «человек» переходит «пассивным» путем, то есть другой агент потребляет его как ресурс в одном состоянии и производит того же агента в другом состоянии (и, возможно, в другом месте). Желтый цвет состояния обозначает текущее состояние агента, зеленая стрелка - активный переход.



3.4 Задача о мусорщиках

Рассмотрим задачу о мусорщиках.

Постановка задачи

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

Цели моделирования и анализа

Предлагается промоделировать данную задачу в нотации TRDA сетей при помощи TRDA Tool.

На примере этой задачи рассмотрим, во-первых, работу временной характеристики - времени Мерлина, и, во-вторых, рассмотрим свойство ограниченности.

Решение

Вершинами системной сети станут: три комнаты, стол и мусорная корзина. Сложными агентами станут генератор предметов и уборщик. Генератор может производить бумагу или мусор, либо отдыхать. Уборщик может или брать бумагу из комнаты и класть бумагу на стол, или брать мусор из комнаты и класть мусор в корзину, или перемещаться в соседнюю комнату (потреблять себя самого из текущей комнаты и производить себя же, но уже в другой комнате в соответствии с портами системной сети).

Перемещение уборщика в соседнюю комнату реализовано с помощью механизма переменных (использованных во входных и выходных термах одного из переходов этого агента).

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

Графическая иллюстрация к данной задаче представлена на рисунке 23 и 24. Подробно на картинке изображена только первая комната, но следует понимать, что во всех остальных комнатах входные/выходные дуги такие же.

Рисунок 23. Иллюстрация к задаче о «мусорщиках»

Рисунок 24 Системная сеть задачи о мусорщиках в TRDA Tool

Время Мерлина

Для моделирования возьмем конфигурацию из приложения 4.1 Данная модель включает применение временной характеристики wait (ожидание срабатывания активного перехода) для некоторых переходов агента «Уборщик».

Начальная имеет следующий вид:

place(room1)

inst(clr1) inst(gen1)

place(room2)

inst(gen2) inst(clr2)

place(room3)

inst(gen3) inst(clr3)

В каждой комнате по одному «Уборщику» и по одному «Генератору».

Загрузим модель и запустим выполнение на 50 шагов - Рисунок 25

Рисунок 25. Временная диаграмма, показывающая время Мерлина

Вывод

Как видно из временной диаграммы, время wait_cl и wait_gen как раз соответствует тем самым искусственным задержкам пребывания в состояниях (в ожидании начала выполнения активного перехода), времени Мерлина. Понятно, что такое время удобно использовать в моделировании, когда, даже если все ресурсы есть в наличии, требуется некоторая задержка, например, для согласования начала выполнения действия.

Ограниченность

Смысловой формулировкой проверяемого свойство ограниченности сделаем ограничение количества предметов в комнате комнаты: в каждой комнате может быть не более 5 экземпляров бумаги и не более 5 экземпляров мусора.

Для первой конфигурации берем входной файл из приложения 4.1

Так же зададим свойства для проверки ограниченности:

bound(room1,paper,5)

bound(room1,garbage,5)

bound(room2,paper,5)

bound(room2,garbage,5)

bound(room3,paper,5)

bound(room3,garbage,5))

Загрузим модель в эмулятор - рис. 26

Рисунок 26. Загружена модель о «мусорщиках»

Поставим галку Ограниченность, выполним (автоматически) произвольные 500 шагов и нажмем кнопку «Результаты анализа» - Рисунок 27

Рисунок 27. Результат анализа ограниченности из приложения 4.1



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

Загрузим модель, выставим галку Ограниченности, запустим 500 произвольных шагов, нажмем «Результаты анализа». - рис 28

Рисунок 28. Результаты анализа ограниченности из приложения 4.2

Тут видно, что за данный прогон количество мусора в комнатах удовлетворяет неравенству:

Количество бумаги в каждой комнате <= 5

Количество мусора в каждой комнате <= 5

Для того, что набрать статистику, запустим еще один экземпляр эмулятора и вновь запустим входной файл (приложение 4.2) и прогоним модель (несколько раз по 500 шагов). - Рисунок 29



Рисунок 29.1. Результаты анализа ограниченности из приложения 4.2

Рисунок 29.2. Результаты анализа ограниченности из приложения 4.2 (многократные прогоны)

Вывод

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

3.5 Задача о курильщиках

Постановка задачи

Имеется три курильщика. У одного из них в кармане есть некоторое количество табака, у другого - бумаги, у третьего - спичек. Имеется стол, на который банкир кладет два из трех ингредиентов курения: либо бумагу и спички, либо спички и табак, либо табак и бумагу. Как только на столе оказывается 2 необходимых ингредиента курения для данного курильщика, он их забирает и начинает курить.

Цели моделирования и анализа

Предлагается проанализировать свойство справедливости - все ли курильщики смогут покурить? Данное свойство будет проверяться с помощью анализа достижимости.

Графическое представление задачи - Рисунок 30

Рисунок 30. Иллюстрации к задаче о курильщиках

Входной файл для данной задачи находится в приложении 5.

Чтобы проанализировать свойство справедливости, зададим следующие параметры анализа достижимости разметки:

marking(m1,like)

place(smoke1)

inst(s1,smoking)

marking(m2,like)

place(smoke2)

inst(s2,smoking)

marking(m3,like)

place(smoke3)

inst(s3,smoking)

Что означает, что мы хотим найти три разметки, в каждой из которых указанный курильщик курит (для каждой из этих разметок не имеет значения, что происходит в других позициях). Загрузим файл в эмулятор, поставим галку «Достижимость» и галку «Паузка при нахождении»

Рисунок 31. Загружена модель о курильщиках

Запустим выполнение на 500 шагов.

Первая остановке представлена на Рисунок 32. Она произошла из-за того, что одна из указанных в параметрах разметка была достигнута (m3).

Рисунок 32. Достигнута первая желаемая разметка в задаче о курильщиках (m3)

Заметим, что это произошло на 12 шаге (см. первую строку результата анализа) и автоматическое выполнение остановилось раньше заданного числа шагов благодаря выставленной галке «Пауза при нахождении»

Идем дальше еще на 500 шагов. - Рисунок 33 - еще одна желаемая разметка (m2) достигнута (но перед этим еще два раза была достигнута m3). Опять же, все это произошло гораздо раньше 500 шагов.

Рисунок 33. Вторая желаемая разметка достигнута (m2)

Идем дальше. - рис.34 - и еще одна желаемая разметка достигнута (m1)

Рисунок 34. Третья желаемая разметка достигнута (m1)

Итак, все желаемые разметки были достигнуты. Результаты анализа можно сохранить в выходной текстовый файл, нажав на кнопку «Сохранить».

Цели моделирования были достигнуты: все курильщики могут покурить.



Заключение

Подводя итог проделанной работе, надо сказать, что поставленная в начале данной работы задача была решена: разработана формальная модель для описания распределенных систем временных автоматов (TRDA модель) и создана инструментальная среда имитационного моделирования на основе данного формализма (TRDA Tool). Разработанный TRDA язык позволяет создавать описание TRDA модели в текстовом файле. TRDA Tool позволяет загружать созданные текстовые файлы на TRDA языке, выполнять имитационное моделирование, как в автоматическом, так и в ручном режиме, как в режиме по шагам, так и во временном режиме. TRDA Tool имеет функции поведенческого и статистического анализа поведения модели, а так же позволяет строить временную диаграмму, благодаря которой можно делать различные выводы о качестве построенной модели. TRDA Tool имеет функцию построения графической картинки как системной, так и автоматной сети загруженной модели. TRDA Tool можно использовать как с русским, так и с английским интерфейсом.

Программный инструмент TRDA Tool имеет свои достоинства и недостатки. Как показали практические эксперименты, многие свойства моделей TRDA сетей могут быть проверены и без построения полного графа покрытия или достижимости. Простое моделирование позволяет акцентировать внимание на деталях, а разумный выбор вероятностей на переходах элементной сети и установка временных параметров увеличивает точность соответствия модели реальным системам.

Однако очевидно, что такие свойства как:

отсутствие живости

отсутствие живости переходов системной сети

ограниченность

недостижимость разметки

отсутствие тупиковой ситуации

могут быть установлены только при наличии полного графа покрытия или достижимости. Это является недостатком реализованных в системе средств анализа.

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

Теперь отметим дальнейшие области развития и применения данного программного инструмента. Наиболее наглядным и полезным свойством, проверяемым данной программой, является достижимость: можно посмотреть как текстовый отчет о результатах автоматического анализа данного свойства, так и его графическое представление (при помощи временной диаграммы). В пояснительной записке не были рассмотрены примеры, где ключевым параметром служило бы время. Однако, очевидно, что в реальных системах всегда присутствует некое время задержки выполнения переходов, по истечении которого необходимые ресурсы могут закончиться, и переход, который 5 минут назад был активным, больше не сможет выполниться. Возможность задания длительности выполнения перехода так же интересна, ведь это позволит оценочно имитировать наиболее длительные бизнес-процессы, после чего их можно будет проанализировать более детально. Надо сказать, что в случае, если функциональность TRDA Tool найдет реальное практическое применение, потребуется реализовать возможность построения моделей графическим способом, интерактивно, через двумерную наглядную схему, содержащую кружочки, стрелочки и т.д., аналогично CPN Tool, в дополнение к используемой сейчас загрузке TRDA-модели из входного текстового файла создаваемого вручную.

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

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

В заключении отметим, что TRDA Tool с теоретическими примерами из пояснительной записки использован в статье «Timed Resource Driven Automata Nets for Distributed Real-Time Systems Modelling», которая принята к выступлению на PaCT-2013 Conference и публикации в LNCS volume Springer Verlag, Germany.



Список использованной литературы

1. R. Alur, D. Dill. A theory of timed automata. Theoretical Computer Science,

2. vol.126(2), 1994. P.183 - 235.

3. V.A. Bashkin. Nets of active resources for distributed systems modeling. Joint

4. Bulletin of NCC&IIS, Comp. Science., vol.28. Novosibirsk, 2008. P.43-54.

5. V.A. Bashkin, I.A. Lomazova. Resource Driven Automata Nets. Fundamenta

6. Informaticae., vol.109(3). 2011. P.223-236.

7. T. Bolognesi, F. Lucidi, and S. Trigila. From timed Petri nets to timed LOTOS.

8. In Proc. of the IFIP WG 6.1 Tenth International Symposium on Protocol Specification, Testing and Verication, 1990. P.1-14.

9. I.A. Lomazova. Nested Petri Nets - a Formalism for Specication and Verication

10. of Multi-Agent Distributed Systems. Fundamenta Informaticae., vol.43(1-4). 2000. P.195-214.

11. P.M. Merlin. A Study of the Recoverability of Computing Systems. PhD thesis,

12. University of California, Irvine, CA, USA, 1974. Automata Network. Int.J. of Algebra and Computation, 14(5-6). 2004. P.719-739.

13. C. Ramchandani. Analysis of asynchronous concurrent systems by timed Petri nets. Technical report. Massachusetts Institute of Technology Cambridge,1974.

14. Reisig W., Rozenberg. Lectures on Petri Nets I: Basic Models, Springer, 1998.

15. UPPAAL Home, Режим доступа: http://www.uppaal.org/, свободный. (дата обращения: 07.01.2013)

16. CPN Tool, Режим доступа: http://cpntools.org/, свободный. (дата обращения: 07.01.2013)

17. ProM, Режим доступа: http://www.promtools.org/prom6/, свободный. (дата обращения: 07.01.2013)

18. Petri Net Markup Language, Режим доступа: http://www.pnml.org/, свободный. (дата обращения: 25.12.2011)



Приложение 1

Задача о философах, гуляющих в парке

model(Dinning_philosophers_wandering)

place(chair1)

place(chair2)

place(chair3)

place(chair4)

place(napkin23)

place(napkin34)

place(dish)

place(napkin12)

place(napkin41)

place(park)

arc_in(chair1,napkin41,getr)

arc_in(chair1,napkin12,getl)

arc_out(chair1,napkin41,putr)

arc_out(chair1,napkin12,putl)

arc_out(chair1,park,ToPark)

arc_in(chair1,chair1,Leave)

arc_out(chair1,chair1,put)

arc_in(chair2,napkin12,getr)

arc_in(chair2,napkin23,getl)

arc_out(chair2,napkin12,putr)

arc_out(chair2,napkin23,putl)

arc_out(chair2,park,ToPark)

arc_in(chair2,chair2,Leave)

arc_out(chair2,chair2,put)

arc_in(chair3,napkin23,getr)

arc_in(chair3,napkin34,getl)

arc_out(chair3,napkin23,putr)

arc_out(chair3,napkin34,putl)

arc_out(chair3,park,ToPark)

arc_in(chair3,chair3,Leave)

arc_out(chair3,chair3,put)

arc_in(chair4,napkin34,getr)

arc_in(chair4,napkin41,getl)

arc_out(chair4,napkin34,putr)

arc_out(chair4,napkin41,putl)

arc_out(chair4,park,ToPark)

arc_in(chair4,chair4,Leave)

arc_out(chair4,chair4,put)

arc_in(chair1,dish,eat)

arc_in(chair2,dish,eat)

arc_in(chair3,dish,eat)

arc_in(chair4,dish,eat)

arc_in(park,park,Leave)

arc_in(park,chair1,get1)

arc_in(park,chair2,get2)

arc_in(park,chair3,get3)

arc_in(park,chair4,get4)

arc_out(park,chair1,ToChair1)

arc_out(park,chair2,ToChair2)

arc_out(park,chair3,ToChair3)

arc_out(park,chair4,ToChair4)

type(fork)

const(f)

port(putr) port(putl) port(getr) port(getl)

type(spag)

const(s)

port(eat)

type(free)

const(free)

port(put) port(get1) port(get2) port(get3) port(get4)

type(philosopher)

state(thinking)

port(Leave) port(ToChair1) port(ToChair2) port(ToChair3) port(ToChair4) port(ToPark)

const(p1) const(p2) const(p3) const(p4)

var(ph)

state_chart_name(LFork_before_eating,1fork)

state_chart_name(RFork_before_eating,1fork)

state_chart_name(RFork_after_eating,1fork)

state_chart_name(LFork_after_eating,1fork)

trans(eating,eating,do_eating) trans_chart_name(eating)

trans_symbol($) priority(60) duration(10)

term_in(eat,s)

trans(eating,LFork_after_eating,L_A) priority(20) duration(1) trans_chart_name(put_fork)

term_out(putr,f)

trans(eating,RFork_after_eating,R_A) priority(20) duration(1) trans_chart_name(put_fork)

term_out(putl,f)

trans(thinking,LFork_before_eating,L_B) duration(2) trans_chart_name(get_fork)

term_in(getl,f)

trans(thinking,RFork_before_eating,R_B) duration(2) trans_chart_name(get_fork)

term_in(getr,f)

trans(thinking,thinking,do_thinking) trans_chart_name(thinking)

duration(5) trans_symbol(?)

trans(thinking,thinking,to_park) duration(2) trans_chart_name(walking)

term_in(Leave,ph,thinking)

term_out(put,free)

term_out(ToPark,ph,thinking)

trans(thinking,thinking,to_chair1) duration(4) trans_chart_name(walking)

term_in(get1,free)

term_in(Leave,ph,thinking)

term_out(ToChair1,ph,thinking)

trans(thinking,thinking,to_chair2) duration(4) trans_chart_name(walking)

term_in(get2,free)

term_in(Leave,ph,thinking)

term_out(ToChair2,ph,thinking)

trans(thinking,thinking,to_chair3) duration(4) trans_chart_name(walking)

term_in(get3,free)

term_in(Leave,ph,thinking)

term_out(ToChair3,ph,thinking)

trans(thinking,thinking,to_chair4) duration(4) trans_chart_name(walking)

term_in(get4,free)

term_in(Leave,ph,thinking)

term_out(ToChair4,ph,thinking)

trans(LFork_before_eating,eating,lets_eat1) trans_chart_name(get_fork)

priority(80) duration(1)

term_in(getr,f)

trans(LFork_before_eating,thinking,lets_think2) trans_chart_name(put_fork)

priority(20) duration(1)

term_out(putl,f)

trans(RFork_before_eating,eating,lets_eat1) trans_chart_name(get_fork)

priority(80) duration(1)

term_in(getl,f)

trans(RFork_before_eating,thinking,lets_think2) trans_chart_name(put_fork)

priority(20) duration(1)

term_out(putr,f)

trans(LFork_after_eating,eating,lets_eat2) trans_chart_name(get_fork)

priority(20) duration(2)

term_in(getr,f)

trans(LFork_after_eating,thinking,lets_think1) trans_chart_name(put_fork)

priority(80) duration(2)

term_out(putl,f)

trans(RFork_after_eating,eating,lets_eat2) trans_chart_name(get_fork)

priority(20) duration(3)

term_in(getl,f)

trans(RFork_after_eating,thinking,lets_think1) trans_chart_name(put_fork)

priority(80) duration(1)

term_out(putr,f)

place(chair1)

inst(p1,thinking)

place(chair2)

inst(p2,thinking)

place(chair3)

inst(p3,thinking)

place(chair4)

inst(p4,thinking)

place(napkin23)

inst(f)

place(napkin34)

inst(f)

place(dish)

inst(s) inst(s) inst(s) inst(s) inst(s) inst(s)

inst(s) inst(s) inst(s) inst(s) inst(s) inst(s)

inst(s) inst(s) inst(s) inst(s) inst(s) inst(s)

inst(s) inst(s) inst(s) inst(s) inst(s) inst(s)

place(napkin12)

inst(f)

place(napkin41)

inst(f)

/* Проверка достижимости */

marking(m1)

place(dish)

inst(s) inst(s)

marking(m2,like)

place(chair3)

inst(p1,thinking)



Приложение 2

Задача о философах и дедлоке

model(Dinning_philosophers_deadlock)

place(chair1)

place(chair2)

place(chair3)

place(chair4)

place(napkin23)

place(napkin34)

place(dish)

place(napkin12)

place(napkin41)

arc_in(chair1,napkin41,getr)

arc_in(chair1,napkin12,getl)

arc_out(chair1,napkin41,putr)

arc_out(chair1,napkin12,putl)

arc_in(chair1,chair1,Leave)

arc_out(chair1,chair1,put)

arc_in(chair2,napkin12,getr)

arc_in(chair2,napkin23,getl)

arc_out(chair2,napkin12,putr)

arc_out(chair2,napkin23,putl)

arc_in(chair2,chair2,Leave)

arc_out(chair2,chair2,put)

arc_in(chair3,napkin23,getr)

arc_in(chair3,napkin34,getl)

arc_out(chair3,napkin23,putr)

arc_out(chair3,napkin34,putl)

arc_in(chair3,chair3,Leave)

arc_out(chair3,chair3,put)

arc_in(chair4,napkin34,getr)

arc_in(chair4,napkin41,getl)

arc_out(chair4,napkin34,putr)

arc_out(chair4,napkin41,putl)

arc_in(chair4,chair4,Leave)

arc_out(chair4,chair4,put)

arc_in(chair1,dish,eat)

arc_in(chair2,dish,eat)

arc_in(chair3,dish,eat)

arc_in(chair4,dish,eat)

type(fork)

const(f)

port(putr) port(putl) port(getr) port(getl)

type(spag)

const(s)

port(eat)

type(free)

const(free)

port(put) port(get1) port(get2) port(get3) port(get4)

type(philosopher)

state(thinking)

port(Leave) port(ToChair1) port(ToChair2) port(ToChair3) port(ToChair4)

const(p1) const(p2) const(p3) const(p4)

var(ph)

state_chart_name(LFork_before_eating,1fork)

state_chart_name(RFork_before_eating,1fork)

state_chart_name(RFork_after_eating,1fork)

state_chart_name(LFork_after_eating,1fork)

trans(eating,eating,do_eating) trans_chart_name(eating)

priority(60) duration(10)

term_in(eat,s)

trans(eating,LFork_after_eating,L_A) priority(20) duration(1) trans_chart_name(put_fork)

term_out(putr,f)

trans(eating,RFork_after_eating,R_A) priority(20) duration(1) trans_chart_name(put_fork)

term_out(putl,f)

trans(thinking,LFork_before_eating,L_B) duration(2) trans_chart_name(get_fork)

term_in(getl,f)

trans(thinking,RFork_before_eating,R_B) duration(2) trans_chart_name(get_fork)

term_in(getr,f)

trans(LFork_before_eating,eating,lets_eat1) trans_chart_name(get_fork)

priority(80) duration(1)

term_in(getr,f)

trans(RFork_before_eating,eating,lets_eat1) trans_chart_name(get_fork)

priority(80) duration(1)

term_in(getl,f)

trans(LFork_after_eating,eating,lets_eat2) trans_chart_name(get_fork)

priority(20) duration(2)

term_in(getr,f)

trans(LFork_after_eating,thinking,lets_think1) trans_chart_name(put_fork)

priority(80) duration(2)

term_out(putl,f)

trans(RFork_after_eating,eating,lets_eat2) trans_chart_name(get_fork)

priority(20) duration(3)

term_in(getl,f)

trans(RFork_after_eating,thinking,lets_think1) trans_chart_name(put_fork)

priority(80) duration(1)

term_out(putr,f)

place(chair1)

inst(p1,thinking)

place(chair2)

inst(p2,thinking)

place(chair3)

inst(p3,thinking)

place(chair4)

inst(p4,thinking)

place(napkin23)

inst(f)

place(napkin34)

inst(f)

place(dish)

inst(s) inst(s) inst(s) inst(s) inst(s) inst(s)

inst(s) inst(s) inst(s) inst(s) inst(s) inst(s)

inst(s) inst(s) inst(s) inst(s) inst(s) inst(s)

inst(s) inst(s) inst(s) inst(s) inst(s) inst(s)

place(napkin12)

inst(f)

place(napkin41)

inst(f)



Приложение 3

Задача о спящем парикмахере

place(street)

place(reception)

place(chair)

arc_in(reception,reception,free)

arc_in(reception,street,man_from_street)

arc_out(reception,reception,man_to_queue)

arc_in(chair,reception,man_from_queue)

arc_out(chair,chair,man_to_chair)

arc_out(chair,reception,free)

arc_in(chair,chair,man_from_chair)

arc_out(chair,street,man_to_street)

type(man)

const(m)

const(m01) const(m02) const(m03) const(m04)

const(m05) const(m06) const(m07) const(m08)

const(m09) const(m10) const(m11) const(m12)

var(x)

port(new_man) port(old_man)

port(man_to_queue)

port(man_from_queue)

port(man_from_chair)

port(man_to_chair)

port(man_from_street)

port(man_to_street)

state(shorn) state(unshorn) state(unshorn_wait) state(shorning)

trans(new_shorn,shorn) duration(1) reset(x) trans_chart_name(after_barber)

trans(shorn,unshorn) duration(1) constr(x>30) reset(y) trans_chart_name(with_new_hair)

type(free)

const(free) port(free)

type(barber)

const(barber)

state(sleep) state(work)

trans(sleep,work) duration(1) reset(x)

term_in(man_from_queue,x,unshorn_wait)

term_out(man_to_chair,x,shorning)

term_out(free,free)

trans(work,sleep) duration(1) constr(x>5)

term_in(man_from_chair,x,shorning)

term_out(man_to_street,x,new_shorn)

type(manager)

const(manager)

trans(s,s) wait(1,2) duration(1) trans_chart_name(take_str_man)

term_in(free,free)

term_in(man_from_street,x,unshorn)

term_out(man_to_queue,x,unshorn_wait)

place(reception)

inst(manager)

inst(free) inst(free) inst(free) inst(free)

place(chair)

inst_viz(barber)

place(street)

inst(m03) inst(m04) inst(m01) inst(m02)

marking(m1,like)

place(chair)

inst(m01,shorning)

inst(barber,work)

marking(m2,like)

place(chair)

inst(m02,shorning)

inst(barber,work)

marking(m3,like)

place(chair)

inst(m03,shorning)

inst(barber,work)

marking(m4,like)

place(chair)

inst(m04,shorning)

inst(barber,work)



Приложение 4

1 Задача о мусорщиках_1

place(room1)

place(room2)

place(room3)

place(basket)

place(table)

arc_in(room1,room1,getp)

arc_in(room1,room1,getg)

arc_in(room1,room1,getc)

arc_out(room1,room1,genp)

arc_out(room1,room1,geng)

arc_out(room1,table,putp)

arc_out(room1,basket,putg)

arc_out(room1,room2,go)

arc_in(room2,room2,getp)

arc_in(room2,room2,getg)

arc_in(room2,room2,getc)

arc_out(room2,room2,genp)

arc_out(room2,room2,geng)

arc_out(room2,table,putp)

arc_out(room2,basket,putg)

arc_out(room2,room3,go)

arc_in(room3,room3,getp)

arc_in(room3,room3,getg)

arc_in(room3,room3,getc)

arc_out(room3,room3,genp)

arc_out(room3,room3,geng)

arc_out(room3,table,putp)

arc_out(room3,basket,putg)

arc_out(room3,room1,go)

type(garbage)

const(g) port(getg) port(putg) port(geng)

type(paper)

const(p) port(getp) port(putp) port(genp)

type(cleaner)

const(clr) const(clr1) const(clr2) const(clr3)

var(x)

port(getc) port(go)

state_chart_name(s,wait_cl)

trans(s,s,clean) wait(1,2) time(2,5) priority(49) trans_chart_name(clean)

term_in(getg,g)

term_out(putg,g)

trans(s,s,org) wait(1,2) time(2,5) priority(49) trans_chart_name(org)

term_in(getp,p)

term_out(putp,p)

trans(s,s,go) wait(1,2) time(10,15) priority(1) trans_chart_name(go)

term_in(getc,x,s)

term_out(go,x,s)

type(generator)

const(gen) const(gen1) const(gen2) const(gen3)

state(s)

state_chart_name(s,wait_gen)

trans(s,s,pap) wait(1,2) time(10,12) trans_chart_name(pap)

term_out(genp,p)

trans(s,s,garb) wait(1,2) time(12,14) trans_chart_name(garb)

term_out(geng,g)

trans(s,s,pause) wait(1,2)

place(room1)

inst(clr1) inst(gen1)

place(room2)

inst(gen2)

inst(clr2)

place(room3)

inst(gen3)

inst(clr3)

bound(room1,paper,5)

bound(room1,garbage,5)

bound(room2,paper,5)

bound(room2,garbage,5)

bound(room3,paper,5)

bound(room3,garbage,5))

.2 Задача о мусорщиках_2

place(room1)

place(room2)

place(room3)

place(basket)

place(table)

arc_in(room1,room1,getp)

arc_in(room1,room1,getg)

arc_in(room1,room1,getc)

arc_out(room1,room1,genp)

arc_out(room1,room1,geng)

arc_out(room1,table,putp)

arc_out(room1,basket,putg)

arc_out(room1,room2,go)

arc_in(room2,room2,getp)

arc_in(room2,room2,getg)

arc_in(room2,room2,getc)

arc_out(room2,room2,genp)

arc_out(room2,room2,geng)

arc_out(room2,table,putp)

arc_out(room2,basket,putg)

arc_out(room2,room3,go)

arc_in(room3,room3,getp)

arc_in(room3,room3,getg)

arc_in(room3,room3,getc)

arc_out(room3,room3,genp)

arc_out(room3,room3,geng)

arc_out(room3,table,putp)

arc_out(room3,basket,putg)

arc_out(room3,room1,go)

type(garbage)

const(g) port(getg) port(putg) port(geng)

type(paper)

const(p) port(getp) port(putp) port(genp)

type(cleaner)

const(clr) const(clr11) const(clr21) const(clr31) const(clr12) const(clr22) const(clr32)

var(x)

port(getc) port(go)

state_chart_name(s,wait_cl)

trans(s,s,clean) wait(1,2) time(2,5) priority(49) trans_chart_name(clean)

term_in(getg,g)

term_out(putg,g)

trans(s,s,org) wait(1,2) time(2,5) priority(49) trans_chart_name(org)

term_in(getp,p)

term_out(putp,p)

trans(s,s,go) wait(1,2) time(10,15) priority(1) trans_chart_name(go)

term_in(getc,x,s)

term_out(go,x,s)

type(generator)

const(gen) const(gen1) const(gen2) const(gen3)

state(s)

state_chart_name(s,wait_gen)

trans(s,s,pap) wait(1,2) time(10,12) trans_chart_name(pap)

term_out(genp,p)

trans(s,s,garb) wait(1,2) time(12,14) trans_chart_name(garb)

term_out(geng,g)

trans(s,s,pause) wait(1,2)

place(room1)

inst(clr11)

inst(clr12)

inst(gen1)

place(room2)

inst(clr21)

inst(clr22)

inst(gen2)

place(room3)

inst(clr31)

inst(clr32)

inst(gen3)

bound(room1,paper,5)

bound(room1,garbage,5)

bound(room2,paper,5)

bound(room2,garbage,5)

bound(room3,paper,5)

bound(room3,garbage,5))



Приложение 5

Задача курильщиках

model(smokers)

place(smoke1) place(smoke2) place(smoke3)

place(pocket1) place(pocket2) place(pocket3)

place(table)

place(bank)

arc_in(smoke1,table,get)

arc_in(smoke2,table,get)

arc_in(smoke3,table,get)

arc_out(smoke1,table,put)

arc_out(smoke2,table,put)

arc_out(smoke3,table,put)

arc_in(smoke1,pocket1,get)

arc_in(smoke2,pocket2,get)

arc_in(smoke3,pocket3,get)

arc_in(bank,table,get)

arc_out(bank,table,put)

type(resource)

const(tobacco) const(paper) const(matches) const(give)

port(get) port(put)

type(smoker)

const(s1) const(s2) const(s3)

state(no_smoking) state_chart_name(no_smoking,no_smoking)

trans(no_smoking,smoking) duration(5) trans_chart_name(smoking)

term_in(get,tobacco)

term_in(get,paper)

term_in(get,matches)

term_out(put,give)

trans(smoking,no_smoking) duration(1) trans_chart_name(no_smoking)

type(banker)

const(banker)

state_chart_name(s,ready)

trans(!matches,s) term_in(get,give) duration(1) trans_chart_name(ready)

trans(!paper,s) term_in(get,give) duration(1) trans_chart_name(ready)

trans(!tobacco,s) term_in(get,give) duration(1) trans_chart_name(ready)

trans(s,!matches)

term_out(put,tobacco)

term_out(put,paper)

duration(1)

trans(s,!paper)

term_out(put,tobacco)

term_out(put,matches)

duration(1)

trans(s,!tobacco)

term_out(put,matches)

term_out(put,paper)

duration(1)

place(table)

inst(give)

place(bank) inst(banker)

place(smoke1) inst(s1)

place(smoke2) inst(s2)

place(smoke3) inst(s3)

place(pocket1)

inst(tobacco) inst(tobacco) inst(tobacco) inst(tobacco)

place(pocket2)

inst(paper) inst(paper) inst(paper) inst(paper) inst(paper)

place(pocket3)

inst(matches) inst(matches) inst(matches) inst(matches) inst(matches) inst(matches) inst(matches)

marking(m1,like)

place(smoke1)

inst(s1,smoking)

marking(m2,like)

place(smoke2)

inst(s2,smoking)

marking(m3,like)

place(smoke3)

inst(s3,smoking)



Приложение 6

Техническое задание

Правительство Российской Федерации

Федеральное государственное автономное образовательное учреждение

высшего профессионального образования

Национальный исследовательский университет

Высшая школа экономики

Факультет бизнес информатики

Отделение программной инженерии

Кафедра «Управление разработкой программного обеспечения»

МАГИСТЕРСКАЯ ДИССЕРТАЦИЯ

Техническое задание

Инструментальная среда имитационного моделирования распределенных систем мобильных агентов

Исполнитель: студентка группы 271мУРПО

___________________ /Новикова Ю.А./

«_____»_______________________ 2013 г.

Руководитель работы:

профессор, доктор физико-математических наук

____________________ / Ломазова И.А./

«_____»_______________________ 2013 г.

Москва 2013

Оглавление

Оглавление90

1.Введение92

2.Основания для разработки92

3. Назначение разработки92

3.1.Функциональное назначение.92

3.2.Эксплуатационное назначение.92

4. Требования к программе92

4.1.Требования к функциональным характеристикам92

4.1.1 Требования к выполняемым функциям92

4.1.2 Графические требования93

4.1.3 Требования к исходным данным93

4.1.4 Требования к выходным данным93

4.2. Требования к надежности94

4.3. Условия эксплуатации94

4.4.Требования к информационной и программной совместимости94

4.5.Требования к составу и параметрам технических средств94

5.Стадии и этапы разработки94

6.Технико-экономические показатели97

7.Порядок контроля и приемки97

8.Требования к программной документации97

Введение

Наименование программы: Инструментальная среда имитационного моделирования распределенных систем временных автоматов.

Основания для разработки

Основанием является тот факт, что данная программа является магистерской диссертацией за второй год обучения в магистратуре отделения программной инженерии факультета бизнес информатики Национального Исследовательского Университета Высшей Школы Экономики.

Организация, утвердившая этот документ - НИУ - ВШЭ, отделение программной инженерии факультета бизнес - информатики, кафедра управление разработкой программного обеспечения.

Наименование темы разработки: магистерская диссертация.

3. Назначение разработки

3.1.Функциональное назначение.

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

3.2.Эксплуатационное назначение.

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

4. Требования к программе

4.1.Требования к функциональным характеристикам

4.1.1 Требования к выполняемым функциям

чтение данных из файла

проведение моделирования

сохранение результатов в файл

вывод справочной информации

анализ и проверка поведенческих свойств моделей

построение временной диаграммы

вывод статической аналитической информации

визуализация системной и автоматной сетей

поддержка двуязычного интерфейса: русский, английский язык

4.1.2 Графические требования

Графическое отражение загруженной модели

Возможность наглядного просмотра поведения (выполнения) модели

Просмотр временной диаграммы длительности состояний сложных агентов

4.1.3 Требования к исходным данным

Требования в исходным данным описаны в Пояснительной Записке, в разделе Разработка языка описания модели типа ресурсно-управляемых сетей временных автоматов.

4.1.4 Требования к выходным данным

Программа должна предоставлять возможность сохранить полученную модель в виде текстового файла. Структура текстового файла должна соответствовать тем же требованиям, предъявляемым к исходному файлу.

При выборе опции по визуализации или системной, или автоматной сети автоматическим образом в директорию, в которой размещен входной файл модели (*.rda) должно сохраняться два файла: построенная модель графа в формате (*.dot) и визуальная картинка модели (*.jpg).

Специальные требования к емкостным характеристикам программы не предъявляются.

4.2. Требования к надежности

синтаксический контроль исходных данных

4.3. Условия эксплуатации

Квалификация эксплуататора программы - пользователь ПК и выше.

4.4.Требования к информационной и программной совместимости

Программа предназначена для работы под операционной системой Windows XP SP2. Кроме того, на компьютере должна быть установлена среда исполнения .NET Framework версии 2.0 или выше. Для работы с визуализацией на компьютере должна быть установлена программа Graphviz 2.28. Программа доступна для скачивания на сайте http://www.graphviz.org/Home.php. После установки программы, требуется перезагрузить операционную систему, для того, чтобы команда dot.exe прописалась в пути (path).

4.5.Требования к составу и параметрам технических средств

Таблица 1 - Требования к составу и параметрам технических средств

№	Необходимый процессор	Рекомендуемый процессор	Необходимое ОЗУ	Рекомендуемое ОЗУ
1	Pentium 1GHz	Pentium 2 GHz или с более высоким быстродействием	1 Gb	2Gb

Стадии и этапы разработки

Таблица 2 - Стадии и этапы разработки

№	Стадии разработки	Этапы работ	Содержание работ
1	Техническое задание	Обоснование необходимости разработки программы	Постановка задачи
			Сбор исходных материалов
		Научно-исследовательские работы	Определение структуры входных и выходных данных.
			Предварительный выбор методов решения задач.
			Определение требований к техническим средствам.
		Разработка и утверждение технического задания	Определение требований к программе.
			Разработка технико-экономического обоснования разработки программы.
			Определение стадий, этапов и сроков разработки программы и документации на неё.
			Выбор языков программирования.
			Согласование и утверждение технического задания.
2	Технический проект	Разработка технического проекта	Уточнение структуры входных и выходных данных.
			Разработка алгоритма решения задачи.
			Определение формы представления входных и выходных данных.
			Разработка структуры программы.
		Утверждение технического проекта	Разработка плана мероприятий по разработке и внедрению программ.
			Разработка пояснительной записки.
			Согласование и утверждение технического проекта.
3	Рабочий проект	Разработка программы	Разработка программы
		Разработка программной документации	Разработка программных документов.
		Испытания программы	Разработка, согласование и утверждение порядка и методики испытаний.
			Корректировка программы и программной документации по результатам испытаний.
4	Внедрение	Подготовка и передача программы.	Сдача программы и программной документации заказчику.

Технико-экономические показатели

От разрабатываемой программы требуется уметь открывать файл модели за период времени в пределах 10 секунд, уметь находить варианты дальнейшего поведения загруженной модели за период времени в пределах 10 секунд.

Порядок контроля и приемки

Контроль и приемка разработки осуществляются в соответствии с документом «Программа и методика испытаний».

Требования к программной документации

В процессе разработки должны быть созданы следующие документы:

текст программы

пояснительная записка

программа и методика испытаний

руководство оператора



Приложение 7

Программа и методика испытаний

Правительство Российской Федерации

Федеральное государственное автономное образовательное учреждение

высшего профессионального образования

Национальный исследовательский университет

Высшая школа экономики

Факультет бизнес информатики

Отделение программной инженерии

Кафедра «Управление разработкой программного обеспечения»

МАГИСТЕРСКАЯ ДИССЕРТАЦИЯ

Программа и методика испытаний

«Инструментальная среда имитационного моделирования распределенной системы мобильных агентов»

Исполнитель: студентка группы 271мУРПО

___________________ /Новикова Ю.А./

«_____»_______________________ 2013 г.

Руководитель работы

Профессор, доктор физико-математических наук

____________________ / Ломазова И.А./

«_____»_______________________ 2013 г.

Москва 2013

1.Объект испытаний

На испытание выносится программа «Инструментальная среда имитационного моделирование распределенной системы временных автоматов» (TRDA Tool).

Программа выполняет следующий набор функций:

Чтение выбранного пользователем входного файла на описанном в ПЗ языке

Построение модели ресурсно-управляемых сетей временных автоматов по входному файлу

Просмотр выполнения построенной модели

Построение временной диаграммы по просмотренным шагам выполнения модели

Сохранение получившейся модели в файл

Проверка поведенческих свойств модели

Вывод статической информации

Визуализация системной и автоматной сети

Поддержка мультиязычности: русский, английские языки

2.Цель испытания

Испытания проводятся с целью проверки работоспособности предъявляемой программы и соответствия ее требованиям технического задания (ТЗ) по составу и функциональным характеристикам.

3.Состав предъявляемой документации

При проведении испытаний предъявляются следующая программная документация:

руководство оператора;

пояснительная записка

код программы (приложения к ПЗ);

техническое задание

4.Технические требования

4.1Требования к программной документации

Состав программной документации:

Имитационная среда имитационного моделирования распределенной системы временных автоматов. Пояснительная записка.

Имитационная среда имитационного моделирования распределенной системы временных автоматов. Код программы.

Имитационная среда имитационного моделирования распределенной системы временных автоматов. Программа и методика испытаний.

Имитационная среда имитационного моделирования распределенной системы временных автоматов. Руководство оператора.

4.2Требования к программе

Программа выполняет следующий набор функций:

Чтение выбранного пользователем входного файла на описанном в ПЗ языке

Построение модели ресурсно-управляемых сетей временных автоматов по входному файлу

Просмотр выполнения построенной модели

Построение временной диаграммы по просмотренным шагам выполнения модели

Сохранение получившейся модели в файл

Проверка поведенческих свойств модели

Вывод статической информации

Визуализация системной и автоматной сети

Поддержка мультиязычности: русский, английские языки

5. Средства и порядок испытаний

Для функционирования программы необходим стандартный комплект оборудования (персональный компьютер) со следующей конфигурацией:

1) Системный блок

- процессор с тактовой частотой не ниже 1ГГц

- 1024Мб ОЗУ

- 40Гб НЖМД

- видеокарта, поддерживающая разрешение 1024х768 и 256 цветов

2) Монитор, поддерживающий разрешение 1024х768 и 256 цветов

3) Клавиатура

4) Мышь

5.2.Программные средства

Программа представляет собой автономный программный продукт, для ее функционирования необходима установленная ОС MS Windows 2000\XP\7\8. Так же необходима установка .NET Framework 2.0. Для работы с визуализацией на компьютере должна быть установлена программа Graphviz 2.28, доступная для скачивания по ссылке: http://www.graphviz.org/Download.php. После установки программы, требуется перезагрузить операционную систему, для того, чтобы команда dot.exe прописалась в пути (path), и стала доступна для выполнения из любой директории.

5.3 Порядок Проведения Испытаний

Испытания должны выполняться в следующем порядке:

Выполнить стандартную процедуру начальной загрузки операционной системы.

Запустить программу. Для этого необходимо запустить файл Automata.exe.

Провести необходимые испытания, описанные в разделе «Методы испытаний».

Выйти из программы

6.Методы испытаний

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

6.1 Испытания общего хода работы программы

Испытание выполняется следующим образом:

Выбрать входной файл с текстом не соответствующим синтаксису разработанного языка (файл -> открыть);

Просмотреть сообщения об ошибке;

Выбрать входной файл с правильным синтаксисом (файл -> открыть) и заданной необходимостью проверки свойства достижимости для одной из позиций

Просмотреть загруженную модель в левой стороне главной формы;

Выставить галочку «Достижимость» на главной форме

Выбрать (выполнить по средствам двойного нажатия) необходимые переходы, представленные в правой стороне главной формы;

Нажать кнопку «Просмотр временной диаграммы»;

Просмотреть форму с цветной диаграммой;

Вернуться на главную форму;

Запустить модель по времени (выбрать значение в выпадающем меню);

Просмотреть результат в левой стороне главной формы;

Нажать кнопку «по шагам»;

Выбрать нужные переходы;

Сохранить результаты выполнения модели в файл (файл -> сохранить);

Нажать кнопку «Результаты анализа»;

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

Просмотреть статистическую информацию об агентах;

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

Выставить галочку «Системная сеть»;

Выставить галочку «Автоматная сеть»;

Просмотреть картинку системной сети;

Просмотреть картинку автоматной сети;

Переключить язык на английский (файл->English/Русский)

Убедиться, что текстовые элементы главной формы переведены на английский язык



Приложение 8

Руководство оператору

Правительство Российской Федерации

Федеральное государственное автономное образовательное учреждение

высшего профессионального образования

Национальный исследовательский университет

Высшая школа экономики

Факультет бизнес информатики

Отделение программной инженерии

Кафедра «Управление разработкой программного обеспечения»

МАГИСТЕРСКАЯ ДИССЕРТАЦИЯ

Руководство оператору

Инструментальная среда имитационного моделирования распределенных систем мобильных агентов

Исполнитель: студентка группы 271мУРПО

___________________ /Новикова Ю.А./

«_____»_______________________ 2013 г.

Руководитель работы:

профессор, доктор физико-математических наук

____________________ / Ломазова И.А./

«_____»_______________________ 2013 г.

Москва 2013

1.Назначение программы

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

Программа предназначена для использования учащимися или преподавателями, или другими заинтересованными лицами с целью визуального просмотра автоматического или пошагового выполнения построенных ими моделей типа «распределенных систем временных автоматов».

2.Условие выполнения программы

Для функционирования программы необходим стандартный комплект оборудования (персональный компьютер) со следующей конфигурацией:

1) Системный блок

- процессор с тактовой частотой не ниже 1ГГц

- 1024Мб ОЗУ

- 40Гб НЖМД

- видеокарта, поддерживающая разрешение 1024х768 и 256 цветов

2) Монитор, поддерживающий разрешение 1024х768 и 256 цветов

3) Клавиатура

4) Мышь

Программа представляет собой автономный программный продукт, для ее функционирования необходима установленная ОС MS Windows 2000\XP\7\8. Так же необходима установка .NET Framework 2.0. Для работы с визуализацией на компьютере должна быть установлена программа Graphviz 2.28, доступная для скачивания по ссылке: http://www.graphviz.org/Download.php. После установки программы, требуется перезагрузить операционную систему, для того, чтобы команда dot.exe прописалась в пути (path), и стала доступна для выполнения из любой директории.

...