Стр. 9 - Программный комплекс верификации алгоритмов программного обеспечения с помощью иерархических сетей Петри

ISSN 2305-5626. Вестник МГТУ им. Н.Э. Баумана: электронное издание. 2013

9

Помимо тупиковых ситуаций, циклов и зацикливаний следует от-

слеживать, все ли части алгоритма выполняются. Под невыполнимы-

ми операциями подразумевают переходы, которые никогда не сраба-

тывают.

Для нахождения таких переходов в процессе построения дерева

достижимости необходимо отмечать переходы, которые могут срабо-

тать. Затем простым пересечением множества всех переходов и мно-

жества переходов, которые могут сработать, получается множество

переходов, до которых выполнение никогда не дойдет.

Функционирование разработанного программного комплекса

можно описать с помощью схемы, приведенной на рис. 6.

Рис. 6. IDEF0-диаграмма функционирования программы

Программный комплекс анализа алгоритмов, формализованных

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

– модуль редактора сети Петри — содержит как графическое

представление сети, так и аналитическое;

– модуль графического редактора — описывает основные функ-

ции любого графического редактора, такие как добавление элемен-

тов, удаление, изменение размера и пр.;

– модуль сети Петри — содержит математическое описание сети,

определение маркировки сети, допустимых переходов и прочие

вспомогательные функции;

– модуль построения дерева достижимости — строит дерево до-

стижимости данной сети Петри;

– модуль анализа дерева достижимости — анализирует постро-

енное дерево применительно к данной предметной области;

– модуль матричного метода — решает задачу достижения неко-

торой маркировки.

Диаграмма модулей и взаимосвязей представлена на рис. 7.