Сотрудники лаборатории ПОИС представили свои работы на конференции TMPA

3–4 марта 2017 года в Москве прошла 4-ая международная научно-практическая конференция инструменты и методы анализа программ TMPA (http://tmpaconf.org/). На ней из лаборатории ПОИС выступили: научный сотрудник Алексей Мицюк и стажёр-исследователь Роман Нестеров

Доклад А. Мицюка по работе Layered Layouts for Software Systems Visualization using Nested Petri Nets (Alexey Mitsyuk and Yaroslav Kotylev)

В докладе был предложен способ отображения (визуализации) в 2.5D моделей программных систем, заданных в виде вложенных сетей Петри. Отображение модели в целом происходит в 3D, а отдельные её составляющие (элементные сети) отображаются с использованием классических 2D алгоритмов. В результате получается слоистое размещение модели в пространстве, которое помогает демонстрировать иерархические свойства модели. Предложенный способ отображения может применяться и для других типов моделей. Разработан прототип, реализующий предложенный способ (исходный код доступен по адресу: https://github.com/yavkotylev/NestedPetriNetsTool).


Доклад Р. Нестерова по работе Compositional Process Model Synthesis based on Interface Patterns (Roman Nesterov and Irina Lomazova)

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