Простой учебный верификатор mcheck

В процессе изучения верификации методом modelchecking некоторый "разрыв" между алгоритмами верификации, использующими модель Крипке, и средствами верификации, использующими входные языки, подобные языкам программирования. Хотя по мере изучения доходят до алгоритмов, используемых средствами верификации (spin, smv), в самом начале изучения очень полезно понять и попробовать самые простые алгоритмы с явным представлением всех состояний.

В университете The University of British Columbia разработали простой учебный верификатор mcheck. Верификатор может быть запущен как апплет или как обычное java-приложение. Верификатор позволяет задать модель Крипке в простом текстовом формате:

{ > 0 1 2 p q
1 0 2 q r
2 2 r
}

Фигурные скобки задают границу описания модели Крипке. В каждой строке содержатся: номер состояния, номера состояний, в которые есть переходы из данного состояния, а также атомарные предикаты, истинные в данном состоянии. Символом '>' обозначается начальное состояние.

Верификатор поддерживает CTL- и LTL-формулы. Формулы могут размещаться в отдельном файле, либо в файле с описание структуры Крипке:

-- model
{ > 0 1 2 p q
1 0 2 q r
2 2 r
}
-- specifications
p U r -- LTL: p until r
F r -- LTL: future r
F G r -- LTL: eventually always r


Верификатор имеет возможность проверки эквивалентности LTL-формул, что можно использовать для самоконтроля при различных формулировках одного свойства, либо упрощении записи формулы.

Заманчиво в этом верификаторе то, что он очень прост сам, а также имеет простую и понятную документацию .