Murphi学习笔记(一)

带参协议验证

  • 带参系统用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

参考博客: 师姐

与自己促膝长谈 与孤独握手言欢

文章名: 《Murphi学习笔记(一)》
文章链接:http://hrhr7.cn/index.php/archives/13/
联系方式:tensor7@163.com
除特别注明外,文章均为Cupidr原创,转载时请注明本文出处及文章链接
Last modification:July 21st, 2019 at 03:57 pm
如果觉得我的文章对你有用,请随意赞赏

Leave a Comment