Модель Крипке

Введём понятие множество атомарных предложений (элементарных высказываний) - предложений, внутренняя структура которых не может изменяться. Атомарные предложения (AP)- это базовые предложения, которые могут быть сделаны.

Выбор множества атомарных предложений APважен, так как он фиксирует базовые свойства, которые могут быть сформулированы для исследуемой программы. Поэтому фиксация множества атомарных предложений может быть названа первой ступенью абстракции. Если, например, не позволить множеству APссылаться на некоторые переменные программы, то ни одно свойство, ссылающееся на эти переменные, не может быть сформулировано, и, как следствие, ни одно такое свойство не может быть проверено.

Моделью Крипке (структурой Крипке)[1]над множеством атомарных предложений APназывается тройка (S, R, Label), где

• S - непустое множество состояний;

• R czS х S - тотальное отношение переходов на S, которое сопоставляет

элементу s ∈ S его возможных потомков;

• Label: S → 2^apсопоставляет каждому состоянию s є Sатомарные предложения Label(s),которые верны в s.

Отношение R ⊂ S ? Sназывается тотальным, если оно ставит в соответствие каждому состоянию sє Sкак минимум одного потомка (Vsє S: Ξs'є S: (s, s') є R).

Иногда требуют, чтобы для модели Крипке был задан набор начальных состояний S₀ ⊂ S.

Путь в модели Крипке из состояния s₀ - это бесконечная

последовательность состояний π = s₀ si s₂... такая, что для всех i ≥ 0 выполняется R(s_i, s_i+1).

Модель Крипке может обеспечить различную степень детализации переходов. Переходы в модели Крипке должны моделировать атомарные переходы исходной программы.

При этом нельзя допускать ситуации, когда модель Крипке содержит состояния, которые не наблюдаются в верифицируемой программе. В этом случае может оказаться, что при верификации будут найдены не существующие ошибки.

Для пояснения приведем пример из книги [1]. Рассмотрим программу с двумя переменными х, у и двумя переходами αи β,которые могут выполняться параллельно:

α: х:= х+ у,

β: у:=у+ х.

В начальном состоянии х = 1 л у = 2. Рассмотрим более детальную реализацию переходов αи β,в которой используются команды ассемблера:

α₀: load R₁, х β₀: load R₂, у

α₁: add R₁, у β₁: add R₂, х

α₂: store R₁, х β₂: store R₂, у

Если в программе выполняется сначала переход а, а затем переход β,то она попадает в состояние x = 3 л у = 5. Если переходы выполняются в обратном порядке, то программа попадает в состояние x = 4 л у = 3. Если же переходы совмещаются в следующем порядке: α₀, β₀, α₁, β₁, α₂, β₂,то в результате она попадет в состояние x = 3 л у = 3.

Пусть состояние x = 3 л у = 3 является ошибочным для программы, и требуется проверить, может ли система оказаться в этом состоянии. Допустим также, что система реализована так, что переходы αи βвыполняются атомарно. В этом случае система не может оказаться в ошибочном состоянии. Однако если построить модель Крипке с более детальными переходами, то в процессе верификации будет найдена ошибка, которой не существует в исходной программе.

Пусть теперь, программа реализована детально, и возможно выполнение последовательности α₀, β₀, α₁, β₁, α₂, β₂.Тогда программа неверна, поскольку может попасть в ошибочное состояние. Однако если построить модель Крипке с использованием лишь переходов αи β, то верификация покажет, что программа верна, но это будет неправильным результатом.

1.7.