Инструмент симуляции и анализа вложенных сетей Петри со временем

Ключевые слова: Вложенные сети Петри, временные сети Петри, моделирование систем, симуляция сетей Петри, сети Петри, проверка моделей, граф классов состояний. В наше время становится все больше и больше различных систем и процессов. Зачастую, в разрабатываемых процессах и системах могут содержаться структурные или логические ошибки. Особенно, если речь идет о сложных системах с динамической иерархической структурой, или системах зависящих от времени. Поэтому необходимы инструменты и методы для анализа подобных систем. Вложенные и временные сети Петри являются удобными формализмами, с помощью которых можно моделировать системы с иерархической структурой, и системы, зависящие от времени соответственно. Однако не существует формализма для создания моделей систем, сочетающих эти два свойства. Такими системами могут являться мультиагентные сети, p2p сети и wireless sensor networks. Также не существует и инструмента, который бы оказывал инструментальную поддержку такого формализма. Данная работа ставит следующие задачи: Разработать формализм, сочетающий вложенные и временные сети Петри, и позволяющий моделировать и анализировать системы с динамической структурой, зависящие от времени, реализовать инструмент, поддерживающий данный формализм и способный производить валидацию модели через симуляцию и реализовать алгоритм model checking для данного формализма, с целью обеспечения возможности первичного анализа моделей, основанных на данном формализме. Для решения данных задач был предложен и определен формализм, названный вложенными сетями Петри со временем (NPNwT). Для этого формализма был расширен инструмент NPNTool и был написан алгоритм симуляции NPNwT сетей. Также для создания model checking инструментария, был расширен алгоритм строительства графа классов состояний, созданный для временных сетей Петри, и реализован CTL model checker.