Стр. 2 - Г.П. Можаров, И.В. Парфилов - Подход к поиску взаимных блокировок в многопоточном программном обеспечении с помощью верификатора SPIN

построения формальной модели ПО и проверки заданных свойств на
данной модели с помощью автоматизированных средств.
Рассмотрим подход к выявлению потенциальных взаимных блоки-
ровок в многопоточных программах, основанный на методе Model
Checking. Он заключается в построении схемы использования по-
токами средств синхронизации, спецификации этой схемы на языке
Promela и ее анализа с помощью верификатора SPIN [5].
Представление основных средств синхронизации на языке
Promela. SPIN — свободно распространяемый пакет программ для
формальной верификации систем [5]. Этот пакет используется глав-
ным образом для верификации моделей асинхронных программных
систем и, в частности, коммуникационных протоколов. Он способен
выявлять в моделях программ взаимную блокировку, недостижимые
участки кода, а также определять выполнимость LTL-спецификаций.
С помощью системы SPIN выполняется проверка не самих программ,
а их моделей. Для построения модели по исходной программе или ал-
горитму пользователь (обычно вручную) строит представление этой
программы на С-подобном входном языке пакета SPIN, носящем
название Promela (Protocol Meta Language). Это представление (про-
грамму на языке Promela) можно считать моделью верифицируемой
программы. Конструкции языка Promela просты, они имеют ясную и
четкую семантику, позволяющую перевести (транслировать) любую
программу на этом языке в систему переходов с конечным числом со-
стояний, которая представляет собой модель переходов подлежащей
верификации программы или алгоритма.
Анализ средств синхронизации основных операционных систем и
языков программирования [6] показывает, что все предоставляемые
средства синхронизации могут быть отнесены к одному из трех при-
митивов синхронизации, таким как исключающий семафор (мьютекс),
сигнальная переменная без памяти (условная переменная) и сигналь-
ная переменная с памятью (семафор). Основные операции над прими-
тивами синхронизации представлены в табл. 1.
Для верификации моделей многопоточных программ с помощью
программного средства SPIN, необходимо представить выделенные
базовые примитивы синхронизации на языке Promela.
Сигнальную переменную с памятью можно реализовать на языке
Promela следующим образом:
byte semA=2;
active proctype P( )
{
/* Уменьшение счетчика сигнальной переменной */
atomic
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 87