Тестирование и контроль качества являются чрезвычайно трудоемкими этапами разработки ПО. Для облегчения этой задачи используются несколько различных техник. Одна из них называется верификацией. Model checking — верификация на базе модели Крипке.
Модель Крипке представляет собой набор \((P, S, R, L)\), где \(P\) – конечное множество высказываний, \(S\) — конечное множество состояний модели, \(R \in SxS\) – переход из одного состояния в другое. \(L \in SхP\) – отношение истинности (высказывание \(P\) в состоянии \(S\) истинно).
Отношение \(R\) будем считать рефлексивным, т.е. \(R(S, S)\) всегда существует.
Набор состояний π, начинающийся в состоянии s, представляет собой бесконечную последовательность состояний \(s_0, s_1,...,\) такую что \(s_0 = s\) и для любого \(i ≥ 0\) выполнено \((s_i s_{i+1})\) представляет собой переход.
В данной модели существует кванторы, применяемые к наборам и к состояниям, с помощью которых образуются формулы (элементарная формула, это высказывание, оно выполняется во всех своих истинных состояниях).
- Af выполняется в состоянии \(s\), если формула \(f\) выполняется для каждого набора, начинающегося в состоянии \(s\);
- Ef выполняется в \(s\), если существует набор, начинающийся в состоянии \(s\), в котором формула \(f\) выполняется.
- Если \(f\) и \(g\) формулы, то
- Gf (Globally) выполняется для набора \(s_0s_1…,\) если для любого \(i ≥ 0\) формула \(f\) выполняется в состоянии \(s_i\);
- fUg (Until) выполняется для набора \(s_0s_1…,\) если существует такое \(i ≥ 0\), что \(f\) выполняется для всех состояний \(s_0;s_1;…; si-1,\) и \(g\) выполняется в состоянии \(s_i\).
Проверить формулу \(f\) – означает найти все состояния, для которых она выполняется. Для произвольной формулы это сделать сложно. Ваша задача проще – проверить формулу E(xU(AGy)), где \(x\) и \(y\) - высказывания.
