УДК 004.4'242
МЕТОД ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ ПАРАЛЛЕЛЬНЫХ ПРОГРАММ С ИСПОЛЬЗОВАНИЕМ СЕТЕЙ ПЕТРИ
А. Н. Ивутин, к.т.н., доцент, заведующий кафедрой ВТ, ТулГУ, Тула, Россия;
orcid.org/ 0000-0003-2970-2148, e-mail: Этот адрес электронной почты защищён от спам-ботов. У вас должен быть включен JavaScript для просмотра.
А. Г. Трошина, к.т.н., доцент кафедры ВТ, ТулГУ, Тула, Россия;
orcid.org/ 0000-0002-4304-2513, e-mail: Этот адрес электронной почты защищён от спам-ботов. У вас должен быть включен JavaScript для просмотра.
Рассматривается задача формальной верификации параллельных программ с использованием математического аппарата теории сетей Петри. Целью работы является формализация методов анализа параллельных программ для автоматизации их верификации. Корректный исходный последовательный программный код требует дополнительной верификации в связи с распределением команд и операций между параллельными потоками, их согласованием и синхронизацией. Результатом некорректного преобразования последовательного кода в параллельный является непредсказуемое поведение программы. Таким образом, основными задачами работы являются разработка методов верификации, а также исправления ошибок в параллельных программах. На основе теории сетей Петри с дополнительными семантическими связями сформированы и доказаны теоремы о соответствии параллельного алгоритма последовательному, разработаны методы исправления ошибок в параллельных алгоритмах.
Ключевые слова: сеть Петри, параллельная программа, эквивалентность сетей, верификация, семантические связи.