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

3 / 18

Метод построения абстрактных моделей, используемых для верификации протоколов…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1 51
интерпретации вида   1 2 ,
k c v v v    где   , cap c k показывает, что элемент 1 v
находится в голове очереди , c элемент 2 v — следующий элемент и т. д., элемент
k v находится в хвосте очереди. Обозначим через  
1 : k c v v    интерпретацию
каналов, присваивающую последовательность 1 k v v каналу с и оставляющую
все остальные каналы неизменными. Интерпретация 0  отображает канал в пу-
стую последовательность ,  т. е.    
0 : , 0. c Chan c len        Обозначим че-
рез   Eval Chan множество всех интерпретаций каналов.
Обозначим через   Cond Var множество логических выражений относи-
тельно переменных v Var [6], а через   , Cond Var Chan — множество логиче-
ских выражений относительно переменных v Var и каналов . c Chan Выра-
жения относительно каналов строятся из вызовов функций (), empty (), nempty
(), full () nfull [7] и их объединения с помощью операторов языка Promela.
Формальная семантика оператора языка Promela с переменными из множе-
ства Var и каналами из множества Chan представляется графом программы
над   , Var Chan — ориентированным графом, ребра которого помечены усло-
виями над элементами  , v c Var Chan  и действиями. Вершины графа про-
граммы носят управляющую функцию: они показывают возможные переходы.
Множество действий будем рассматривать как объединение , Act Comm
элементы которого определяются только шестью базовыми операторами языка
Promela: 1) присваивание; 2) оператор assert; 3) оператор print; 4) выражение;
5) отправка сообщения в канал; 6) извлечение сообщения из канала. Действия,
выраженные первыми четырьмя операторами, составляют множество . Act
Действия, выраженные последними двумя операторами, являются коммуника-
ционными действиями:
     
{ ! , ? | , , , }. Comm c v c x c Chan v dom c x Var dom x dom c    
Графом программы (program graph) PG над  
, Var Chan называется шестерка
 
0 0 , , , , , , PG Loc Act Effect Loc g  
где Loc — множество состояний (вершин) графа;   : Effect Act Eval Var 
  Eval Var  — функция, определяющая результат действий; Loc  
    , Cond Var Chan Act Comm Loc     — отношение переходов; 0 Loc Loc —
множество начальных состояний;  
0 , g Cond Var Chan — начальное условие.
Переход  
, , , l g act l  будем сокращенно обозначать
:
.
g act
l l Логическое
условие g называется защитой перехода
:
.
g act
l l Действие act может быть осу-
ществлено только в том случае, если защита g истинна, а действие выполнимо.
Далее будем подразумевать соответствие графов программы Promela-
процессам.