Promela初探 - rqdmap

由于要处理协议分析的大作业，接触了spin和Promela，下面整理一些内容作为记录。

基础语法

参考资料：

数据类型

内置的基础类型有：bit(u1), bool(u1), byte(u8), short(16), int(32)等，这里前缀u表示无符号数。

声明一个变量可以类Ctypename name [ = anyexpr ]), 也可以使用这种语法unsigned name : constant [ = anyexpr ], 这样将声明一个占用conststant位的无符号数。当初始化的值超出了数据类型能表示的范围后，数值将会被截断造成信息的损失，spin只会在随机或指定的模拟下会警告该情况。

用户可以使用关键字mtype定义自己的数据类型，比较类似C语言的枚举类型。

Text

1mtype = { ack, nak, err, next, accept }
2
3init {
4	mtype x = nak;
5	printm(x);
6	printf("%e", x)
7}

这种mtype的定义其实等价于：

Text

1#define	ack	5
2#define nak	4
3#define	err	3
4#define next	2
5#define accept	1

由于这些类型用一个无符号字符存储，因而在一个mtype中最多定义255个不同的类型。

当希望定义多个mtype时可以加上名称，如：

Text

 1mtype { one, two, three }
 2mtype:fruit = { appel, pear, banana }
 3mtype:sizes = { small, medium, large }
 4...
 5init{
 6	mtype a;
 7	mtype:fruit b;
 8	mtype:sizes c;
 9	...
10}

原子操作 atomic

atomic { sequence } 使得指令序列不可分割地执行。

断言 assert

assert(any_boolean_condition)

管道 chan

语法

Text

1chan name
2chan name = '[' const ']' of { typename [, typename ]* }

一个管道必须要初始化后才能传输消息。

Text

1// 创建一个用于16个容量的short类型的管道
2chan a = [16] of { short }
3
4//创建一个同步管道
5chan b = [0] of { mtype }
6
7//创建一个数据类型拥有4个域地管道
8chan qname = [8] of { mtype, int, chan, byte }

消息收发

发送消息

语法

Text

1name ! send_args
2name !! send_args

对一个有缓冲区的未满管道发送消息是可执行的，也可以通过spin添加参数-m使得对有缓冲区的管道发送消息总是可行的，当管道满时，多余的消息将会丢失。

对于有缓冲区的管道而言，第一种方式将会把消息插入到管道尾，保持FIFO的顺序；第二种方式则会按照数值大小插入，保证管道队列有序，如：

Text

1chan x = [4] of { short };
2
3active proctype tester()
4{
5	x!!3; x!!2; x!!1; x!4;
6	x?1; x?2; x?3; x?4
7}

按照这种方式插入，则能按照1234的顺序取出对应的数值。

接受消息

语法

Text

1name ? recv_args
2name ?? recv_args
3name ?< recv_args >
4name ??< recv_args >

第一种和第三种只有当管道第一条消息与对应的参数匹配时才可执行。

第二种和第四种当管道中任意位置存在一条消息与对应的参数匹配时即可执行。

无尖括号的方式在取完消息后清除消息队列中对应的消息，有尖括号的方式则保留不动。

Text

 1chan set = [8] of { byte };
 2byte x;
 3
 4set!!3; set!!5; set!!2;	/* sorted send operations   */
 5
 6set?x;			/* get first element        */
 7if
 8:: set?<x> 		/* copy first element       */
 9:: set??5		/* is there a 5 in the set? */
10:: empty(set)
11fi

这段代码有序插入235三个字节，首先取出队头的2，接下来进入分支选择：只有当set为空时会进入分支3，当队伍中存在5时进入分支2，当队伍至少有一个元素时会进入分支1，同时元素不被删除、队头元素被保存在x。

目前上述的匹配是指数据类型的匹配，不然有很多事情无法解释并且变得匪夷所思。。

Timeout

Timeout变量是一个预定义的、全局的可读布尔变量，当整个系统中没有任何一个语句可执行时该变量为true,其余时间则为false

进程

定义一个进程 使用关键字proctype, proctype name ( [ decl_lst ] ) { sequence } 类似C函数定义的方式，进程之间异步运行。

运行一个进程 run name ( [ arg_lst ] )即可

控制语句

条件选择语句

if :: sequence [ :: sequence ]* fi

循环语句，通过break分支结束运行。

do :: sequence [ :: sequence ]* od

无条件跳转, name即为标签名，类似C语言。

goto name

::后跟的代码序列均为可能的运行选择，由spin随机选择某一段执行。比如下述代码就很好玩。

Text

1int count;
2proctype counter(){
3	do
4	:: count++
5	:: count--
6	:: (count == 0) ->
7		break
8	od
9}

Spin模拟Go-Back-N协议

内容是自己实现的，100%有理解不到位的地方和各种奇怪的BUG。

两天rush出来的，只能说做个垃圾的入门。。。内容懒得整理了，给上实验报告吧。。