ИАПУ ДВО РАН

Построение сокращённого дерева достижимости для моделей программ в терминах сетей Петри


2022

Леонтьев Д. В., Харитонов Д. И.

Системы и средства информатики

Статьи в журналах

23-35

Леонтьев Д.В., Харитонов Д.И. Построение сокращённого дерева достижимости для моделей программ в терминах сетей Петри // Системы и средства информатики. 2022. Т. 32, №2. С. 23-35. https://doi.org/10.14357/08696527220203.

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

10.14357/08696527220203

http://mi.mathnet.ru/ssi824