Подход к статической верификации многопоточных приложений на основе графовых моделей программы

Подход к статической верификации многопоточных приложений на основе графовых моделей программы

Крюков О.С. (ТулГУ, Тула, Россия)
Волошко А.Г. (ТулГУ, Тула, Россия)
Ивутин А.Н. (ТулГУ, Тула, Россия)

Аннотация

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

Ключевые слова

статическая верификация; параллельные программы; сеть Петри; состояние гонки; взаимная блокировка; анализ модели.

Издание

Труды Института системного программирования РАН, том 38, вып. 6, часть 1, 2026, стр. 41-62.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(6)-3

Для цитирования

Крюков О.С., Волошко А.Г., Ивутин А.Н. Подход к статической верификации многопоточных приложений на основе графовых моделей программы. Труды Института системного программирования РАН, том 38, вып. 6, часть 1, 2026, стр. 41-62. DOI: 10.15514/ISPRAS-2026-38(6)-3.

Полный текст статьи в формате pdf Вернуться к содержанию тома