Методы верификации программного обеспечения

3.3.6. Методы и инструменты проверки моделей 
Проверка моделей (model checking) [114] используется для проверки 
выполнения набора свойств, записанных в виде утверждений какого-либо логико-
алгебраического исчисления на исполнимой модели, моделирующей определенные 
проектные решения или код ПО. 
Чаще всего для описания проверяемых свойств используется некоторая 
временная логика или 

-исчисление, а в качестве модели, свойства которой 
проверяются, выступает конечный автомат, состояния которого соответствуют наборам 
значений элементарных формул в проверяемых свойствах, обычно он называется 
моделью Крипке. Проверку модели выполняет специализированный инструмент, 
который либо подтверждает, что модель действительно обладает заданными 
свойствами, либо выдает сценарий ее работы, в конце которого эти свойства 
нарушаются, либо не может прийти к определенному вердикту, поскольку анализ 
модели требует слишком больших ресурсов. 
Проверяемые свойства обычно разделяют на свойства безопасности (safety 
properties), означающие, что нечто нежелательное при любом варианте работы системы 
никогда не случается, и свойства живучести (liveness properties), означающие, 
наоборот, что что-то желательное рано или поздно произойдет. Иногда дополнительно 
выделяют свойства стабильности (или сохранности, persistence properties) — при 

---

64 
любом сценарии работы системы заданное утверждение в некоторый момент 
становится истинным и с тех пор остается выполненным — и свойства справедливости 
(fairness properties) — некоторое утверждение при любом сценарии работы будет 
выполнено в бесконечном множестве моментов времени. Те или иные свойства 
справедливости, например, что планировщик операционной системы после любого 
заданного момента времени гарантирует каждому активному процессу получение 
управления, часто являются исходными предположениями, при выполнении которых 
нужно проверить свойства безопасности или живучести. 
Первые методы проверки моделей [170], предложенные в начале 1980-х, 
предполагали полное исследование моделей Крипке с помощью автоматического 
инструмента, для проверки формул логики ветвящегося времени CTL [171] был 
предложен достаточно эффективный алгоритм. Впоследствии были разработаны 
символические методы [172], в которых проверка выполняется за счет манипуляций с 
компактным представлением модели в виде упорядоченной двоичной разрешающей 
диаграммы (OBDD), что позволяет проверять модели с огромным (до 10
200
) 
количеством состояний. Однако не всякую систему можно представить достаточно 
компактным образом, например, размер OBDD автомата, описывающего умножение 
двоичных чисел, растет экспоненциально в зависимости от разрядности чисел. 
Оказалось, что для некоторых видов временных логик проверочные алгоритмы 
неэффективны — для LTL [173] и CTL* [174] они линейны в зависимости от размера 
автомата, равного максимуму из числа состояний и числа переходов, но являются 
PSPACE-полными в зависимости от длины проверяемой формулы. Для 

-исчисления 
был найден алгоритм проверки моделей [175], сложность которого выражается 
формулой O((S

)
d/2
T

), где S — число состояний модели, 

— длина проверяемой 
формулы, T — размер модели, а d — количество вложенных чередований операторов 
наибольшей и наименьшей неподвижной точки в 

. Большинство исследований 
ведется в направлении поиска различных фрагментов 

-исчисления, в которых можно 
было бы использовать более эффективные алгоритмы. 
Среди инструментов проверки моделей для верификации ПО наиболее широко 
используются следующие. 

---

65 

SPIN [176,177], использующий в качестве моделей описанные на языке Promela 
системы взаимодействующих автоматов. 

Evaluator [178], входящий в состав набора инструментов CADP [179] для 
формального анализа протоколов и распределенных систем. 

SMV [180] и его развитие NuSMV [181] реализуют символическую проверку 
моделей. 

Design/CPN [182], использующий в качестве моделей размеченные сети Петри. 

UPPAAL [183] и Kronos [184], инструменты проверки моделей, используемые 
для верификации встроенных систем и систем реального времени. Оба основаны 
на расширенных временных автоматах, а Kronos еще позволяет использовать 
логику с явным временем для описания проверяемых свойств. 

Bogor [185], один из недавно появившихся инструментов, который, однако, 
активно используется в практических проектах. 

HyTech [186], инструмент для проверки гибридных моделей, используемых при 
создании встроенного ПО.