带参协议验证

• 带参系统用P(N)表示

  • P = protocol

  • N = 参数的个数

    • 参数：具有相同结构的并发执行的主体或者有限个结构不同的主体
• 当N被具体赋值时，就是这个带参系统的一个实例
• 每个主体都能通过规则进行交互
• 规则集R: 刻画带参系统的运行过程
• 相当于每个主体是一个进程，进程之间通过规则进行状态迁移，所有可能发生的事情，都是进程从初始状态通过规则集R中的规则，所到达的状态。带参系统通过调整参数来增加进程，通过验证器来保证某个待验证系统的所有可达状态都是正确的。

Murphi的结构

• 常量，类型，全局变量和过程的定义
• 状态迁移规则的集合
• 初始状态的描述W
• 不变量

Murphi的行为部分，是一个状态迁移规则的集合，每一条规则都是一条保护命令，其由一个条件(全局变量上的布尔表达式)和一个动作(一条可以修改变量的值的语句)组成，条件和动作均用类似于Pascal的风格书写，动作可以是包含循环和条件的任意语句，但不管动作多么复杂，动作的执行都是原子性的。

Murphi验证系统的步骤

• 编写Murphi语言程序，以 *.m 命名。

• 运行Murhpi编译器，将 .m 编译成 .c 或者*.cpp文件

  ./mu *.m

• 运行C++编译器，将 .c 或者.cpp文件进行编译

  g++ -ggdb -o *.o *.cpp -I ../include -lm 

• 运行*.o文件来验证过程

  ./*.o

参考博客: 师姐