Метод построения абстрактных моделей, используемых для верификации протоколов когерентности кэш-памяти масштабируемых систем

10 / 18

В.С. Буренков, С.Р. Иванов
58 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1
так, что множество    
1, , .
k abs opc opc dom m opc   содержит все возможные
значения, которые в исходной модели могли быть отправлены с помощью соот-
ветствующих операторов отправки сообщения, находящихся в 3 , , .
n PG PG
Здесь _ guard abs получается согласно преобразованиям выражений.
Если оператор находится внутри действия защищенной команды do-цикла, то в
цикл добавляется множество защищенных команд, защита которых получается из
защиты исходной команды заменой истиной всех условий относительно канала , c
а действия формируются присваиваниями . ; . ,1 .
i m opc opc m id ABS i k   
Математическое доказательство корректности процедуры абстракции. Про-
верка выполнимости свойств-инвариантов для данной системы переходов TS эк-
вивалентна проверке выполнения свойства p в каждом состоянии, достижимом из
некоторого начального состояния системы . TS Покажем, что множество достижи-
мых состояний системы  
, , , , ,
abs abs abs abs abs abs TS S Act I AP L   включает в себя
множество достижимых состояний системы   , , , , , . TS S Act I AP L  
Теорема. Пусть p — некоторая формула пропозициональной логики, со-
ставленная относительно атомарных высказываний из множества . AP Для
всех состояний , s S таких, что s достижимо из некоторого начального со-
стояния 0 s I и | , s p существует состояние   ,
abs f s S достижимое из не-
которого начального состояния  0 ,
abs f s I  такое, что   | . f s p 
◄ Обозначим множество состояний системы переходов , TS достижимых из
некоторого начального состояния, через   . Reach TS Докажем утверждение
теоремы методом математической индукции по длине пути исходной системы
TS [6].
Базис индукции. Длина пути 0. m  По построению абстракции каждому со-
стоянию s I соответствует состояние   ,
abs f s I такое, что      .
abs L f s L s 
Индуктивная гипотеза. Пусть для некоторого 0 m  верно
   
: .
k abs k m f s Reach TS    Это означает, что фрагменту пути 0 1 m s s s си-
стемы TS соответствует фрагмент пути      
0 1 m f s f s f s  системы ,
abs TS
причем  i f s и  1 ,
i f s  0 , i m   не обязательно различны. Кроме того,
     ,
abs m m L f s L s  0. m 
Шаг индукции. Рассмотрим переход 1 m m s s   исходной системы. Состояние
1 m s  исходной системы TS является следствием наличия в системе перехода из
состояния ,
m s описываемого одним из правил (1)–(3). Рассмотрим все возможные
правила и проверим наличие соответствующих правил в абстрактной системе.
Случай 1. Интерливинг для , 0 .
i Act i n    Элемент множества правил
исходной системы   |0
concrete i Rulesi ric i n    имеет вид
  :
0 1 0
, | ,
, , , , , , , , , , , ,
g
i i
i
m i n m i n
l l g
ric
s l l l s l l l



    

             
где  
, . Effect    