Automated analysis of DP-systems using timed-arc Petri nets via TAPAAL tool

Сети Петри с временными дугами – это временное расширение сетей Петри (TaPN-сети), которое позволяет присваивать таймеры фишкам. Система динамических точек на метрическом графе (DP-система) это другая динамическая модель, которая рассматривается в теории геометрических дискретных динамических систем и, исторически, ее изучение мотивировано изучением распространения локализованных гауссовых волновых пакетов по тонким структурам; кроме того, DP-системы могут использоваться для приближенного представления динамики распространения сообщений в распределенных системах. В этой работе, мы описываем новый подход для автоматического анализа DP-систем используя трансляцию в TaPN сеть, которая реализована как расширение инструмента TAPAAL. Подход позволяет использовать мощные инструменты верификации (TAPAAL/UPPAAL) для анализа динамических характеристик DP-систем, представленных на языке TCTL. В работе продемонстрировано, как можно кодировать временно-темпоральные свойства DP-систем в рамках предложенного подхода, и приведены результаты экспериментальных тестов.