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

Рис. 1. Отчет о верификации модели
Одним из преимуществ подхода к верификации на основе метода
Model Checking является то, что в случае невыполнения требуемых
свойств будет предоставлен контрпример, нарушающий выполнение
заданных свойств. Этот контрпример весьма полезен при поиске оши-
бок в реальной системе. При верификации свойства отсутствия вза-
имных блокировок в модели многопоточной программы таким контр-
примером является очередность выполнения потоков, приводящая к
их взаимной блокировке. На рис. 2 показана динамика работы пото-
ков, при которой происходит взаимная блокировка.
Рис. 2. Контрпример
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 93