论文部分内容阅读
摘要：模型检查工具SPIN的核心是PROMELA语言，对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。该文从语义角度研究了 PROMELA语义引擎问题。首先给出PROMELA语法的抽象对象模型形式化定义，然后给出一个算法来实现PROMELA语法到抽象对象模型的映射，描述 了PROMELA指称语义。
关键词：模型检查；SPIN；PROMELA；语义
中图分类号：TP315文献标识码：A文章编号：1009-3044(2008)35-2159-02
Research on execution patterns of SPIN Semantics Engine
FENG Yan-qing
(School of Information and Technology, Jiangxi University of Finance and Economics, Nanchang 330013, China)
Abstract: The PROMELA language, whose commitment manners decide system executions, plays crucial role in model checking toolSPIN. This paper studies semantic engines of PROMELA. Firstly, a formal model of PROMELA is given. Secondly, the denotational semantics of PROMELA are described by the mapping between syntax of PROMELA and the model. We discuss the specific issuessuch as atomic sequence, rendezvous channel, and their solutions. Finally a case study demonstrates PROMELA workingprinciple.
Key words: model checking; SPIN; PROMELA; semantics
1 引言
模型检查[1-2]在软件开发中扮演非常重要的作用，模型检查的基本思想是使用标记迁移系统（LTS）结构Μ=(S,R,L)描述软件规格模型，使用时态逻辑描述软件应具备的特性ϕ，如活性、安全性和无死锁等，然后使用一个算法检查Μ,s|=ϕ，如果成立表示系统具备所描述特性。
SPIN[3]是功能强大、业界普遍使用的模型检查工具，对SPIN语言PROMELA语义的研究有助于更好地描述系统行为。
本文的目的是给出PROMELA语言的语义解释。文中第二部分首先给出与PROMELA语言元素对应模型对象的形式化定义，然后给出一个算法来实现PROMELA语句到该模型的映射。
2 PROMELA的语义引擎
PROMELA语义引擎[4]决定了PROMELA描述的模型如何被解释和执行。PROMELA语法由变量Variable、消息Message、消息通道Message Channel、进程Procress等部分构成。我们先给出这些语法对应模型的形式化定义，然后给出一个算法来实现PROMELA语句到模型的映射。
2.1 PROMELA语义模型
定义1：Variable（变量）
Variable是一个五元组(name,scope,domain,inival,curval)。name为变量标识符；scope指定变量的作用范围，有全局和局部范围之分；domain表示变量的值域；inival表示变量的初始值；curval表示变量的当前值。Variable的作用范围可以是全局的或是局部的。对于特定的进程来说，变量的类型通常决定变量的值域。
定义2：Message (消息)
Message是Variable（变量）的一个有序集合，表示进程间所交换的数据。
定义3：Message Channel（消息通道）
Message Channel是一个三元组(ch_id,nslots,contents)；ch_id是通道标识符；nslots表示消息通道中最多可以存储的消息数；contents是消息的一个有序集合。消息通道没有定义作用范围，一个消息通道作用范围总是全局的。理论上每一个活动进程都可以通过ch_id进行存取。
定义4：Procress（进程）
Procress是一个六元组(pid,lvars,lstates,initial,curstate,trans)；pid是进程标识符；lvars表示进程的局部变量有限集；lstates表示进程的局部状态有限集；initial表示进程的初始状态；curstate表示进程的当前状态；trans表示进程中所有迁移的有限集；进程处于初始化状态时有curstate= initial,，对于局部变量有curval=inival。
定义5：Tramstion（迁移）
进程中的Tramstion是一个七元组(tr_id,source,target,cond,effect,prty,rv)；tr_id是迁移标识符；source和target分别表示迁移的源状态和目标状态；cond是关于全局系统状态的一个布尔条件；effect函数作用于全局系统状态，它可以修改全局系统状态；prty表示迁移的优先级，PROMELA中迁移的优先级由unless结构定义； rv表示迁移是同步通信(Rendezvous Channel)的接收消息操作。
定义6： System State（全局系统状态）
全局系统状态是元组(gvars,procs,chans,exclusive,handshake,timeout,else,stutter)；gvars表示全局变量有限集；procs表示进程的有限集；chans表示消息通道的有限集；exclusive默认值为0， 当atomic序列中的迁移执行时，会置exclusive为p.pid；handshake标志当前系统状态下有无同步通信发生；布尔变量timeout提供了从系统阻塞状态跳离的方法，仅当所有活动进程中没有可执行迁移时它为true，否则它一直为false；布尔变量else当且仅当当前进程局部状态下进程中没有可执行性迁移时为true；stutter是布尔值，用来确定stutter规则是否起作用；在初始系统状态，所有的进程位于其初始状态，所有的全局变量满足curval=inival；所有的消息通道满足contents={}，exclusive 和handshake为0，timeout、else和stutter初始值为false。
定义1到定义6给出了PROMELA语言中抽象对象的形式化定义，这些抽象对象的关系如图1所示。
2.2 PROMELA语句到语义模型的映射算法
下面我们探讨具体的算法。
第一步：我们考察在系统状态为s时，如何形成关于s的所有状态空间。令元组(p,t)表示对应于系统状态s时p进程及p中的一条可执行迁移t；集合E为二元组(p,t)的集合，它表示在系统状态s下的所有活动进程的所有可能迁移，即求得在系统状态s下的所有可能迁移状态。算法executable( State s)输入给定系统状态 和所有活动进程，输出集合E。executable(s)算法如下所示。
1 executable(State s)
2 {new Set E //创建关于元组(p,t)的集合E
3new Set e //创建关于元组(p,t)的集合e，中间变量
4E = {}
5timeout = false
6AllProcs:
7for each active process p
8 { if (exclusive == 0 //表示当前系统没有迁移处于atomic序列
9 orexclusive == p.pid) //检查进程p中atomic序列中的语句正在执行
10 { for u from high to low // 依P中迁移t优先级从高到低进行
11 { e = {};else = false
12 OneProc: for each transition t in p.trans
13 {if (t.source == p.curstate
14andt.prty == u
15andeval(t.cond) == true
16and(handshake == 0
17or handshake == t.rv) )
18{ add (p,t) to set e }
19}
20if (e != {}) //进程P中当前优先级下有可执行迁移
21{ add all elements of e to E //将可执行迁移t加入到E中
22break //结束优先级检查循环
23}
24else if (else == false) //进程P中当前优先级下无可执行迁移
25 { else = true //置else为true
26 goto OneProc //重新对p中迁移进行可执行性检查
27 }
28}
29}
30 }
31if (E == {} and exclusive != 0) //表示atomic序列中迁移已经执行完毕
32{ exclusive = 0 //重置exclusive为0并重新检查所有活动进程
33goto AllProcs
34}
35if (E == {} and timeout == false) //系统中无可执行迁移，重新进行选择
36{ timeout = true
37goto AllProcs //重新检查所有活动进程
38}
39return E //返回关于系统状态s的所有可能执行迁移(p,t)
40 }
进程p中atomic序列中的迁移执行时，算法置系统变量exclusive为p.pid。在算法executable(s)中atomic序列是如下处理的：算法首先测试系统变量exclusive的值（算法第8、9行）以确保atomic序列中的迁移执行不被中断，然后再执行其它测试。当atomic序列中的所有迁移都执行完毕后，应重置系统变量exclusive并检查所有活动进程（算法第32、33行）。
第二步：我们考察PROMELA语义引擎随机挑选路径对全局系统状态s影响。只要集合E不空，我们在E中随机选择一个二元组(p,t)并执行元组中的可执行迁移t，于是全局系统状态会迁移到新状态s'，t所属进程p的局部状态也会发生迁移；当集合E为空，系统停止运行。特别的，对应于S=S0，系统处于初始状态，所有的进程Pi(i≥0)也处于初始状态。
3 结束语
本文描述了PROMELA语法元素对应的语义模型，并通过算法描述了PROMELA随机交叉执行方式的工作原理。算法的关键是处理PROMELA中atomic序列和同步通信问题，即通过对PROMELA语义模型中的handshake处理，实现将同步通信的发送消息操作和接受消息操作看作一个完整的动作。通过对exclusive的处理，实现atomic序列的执行不会被其它语句随机交叉。理解PROMELA语义引擎的工作原理，将有助于我们理解模型检查工具SPIN是如何对分布式并发系统进行建模和验证的。
参考文献：
[1] Ben-ari M.Principles of the Spin Model Checker[M].London:Springer-Verlag,2008.
[2] Baier C,Katoen J.Principles of Model Checking[M].London,England:The MIT Press,2008.
[3] Holzmann,J G.Spin Model Checker:Primer and Reference Manual[M].Addison-Wesley Professional:2003.
[4] 黎升洪,缪淮扣.时态逻辑描述能力比较研究[J].计算机工程与应用,2006(22).
关键词：模型检查；SPIN；PROMELA；语义
中图分类号：TP315文献标识码：A文章编号：1009-3044(2008)35-2159-02
Research on execution patterns of SPIN Semantics Engine
FENG Yan-qing
(School of Information and Technology, Jiangxi University of Finance and Economics, Nanchang 330013, China)
Abstract: The PROMELA language, whose commitment manners decide system executions, plays crucial role in model checking toolSPIN. This paper studies semantic engines of PROMELA. Firstly, a formal model of PROMELA is given. Secondly, the denotational semantics of PROMELA are described by the mapping between syntax of PROMELA and the model. We discuss the specific issuessuch as atomic sequence, rendezvous channel, and their solutions. Finally a case study demonstrates PROMELA workingprinciple.
Key words: model checking; SPIN; PROMELA; semantics
1 引言
模型检查[1-2]在软件开发中扮演非常重要的作用，模型检查的基本思想是使用标记迁移系统（LTS）结构Μ=(S,R,L)描述软件规格模型，使用时态逻辑描述软件应具备的特性ϕ，如活性、安全性和无死锁等，然后使用一个算法检查Μ,s|=ϕ，如果成立表示系统具备所描述特性。
SPIN[3]是功能强大、业界普遍使用的模型检查工具，对SPIN语言PROMELA语义的研究有助于更好地描述系统行为。
本文的目的是给出PROMELA语言的语义解释。文中第二部分首先给出与PROMELA语言元素对应模型对象的形式化定义，然后给出一个算法来实现PROMELA语句到该模型的映射。
2 PROMELA的语义引擎
PROMELA语义引擎[4]决定了PROMELA描述的模型如何被解释和执行。PROMELA语法由变量Variable、消息Message、消息通道Message Channel、进程Procress等部分构成。我们先给出这些语法对应模型的形式化定义，然后给出一个算法来实现PROMELA语句到模型的映射。
2.1 PROMELA语义模型
定义1：Variable（变量）
Variable是一个五元组(name,scope,domain,inival,curval)。name为变量标识符；scope指定变量的作用范围，有全局和局部范围之分；domain表示变量的值域；inival表示变量的初始值；curval表示变量的当前值。Variable的作用范围可以是全局的或是局部的。对于特定的进程来说，变量的类型通常决定变量的值域。
定义2：Message (消息)
Message是Variable（变量）的一个有序集合，表示进程间所交换的数据。
定义3：Message Channel（消息通道）
Message Channel是一个三元组(ch_id,nslots,contents)；ch_id是通道标识符；nslots表示消息通道中最多可以存储的消息数；contents是消息的一个有序集合。消息通道没有定义作用范围，一个消息通道作用范围总是全局的。理论上每一个活动进程都可以通过ch_id进行存取。
定义4：Procress（进程）
Procress是一个六元组(pid,lvars,lstates,initial,curstate,trans)；pid是进程标识符；lvars表示进程的局部变量有限集；lstates表示进程的局部状态有限集；initial表示进程的初始状态；curstate表示进程的当前状态；trans表示进程中所有迁移的有限集；进程处于初始化状态时有curstate= initial,，对于局部变量有curval=inival。
定义5：Tramstion（迁移）
进程中的Tramstion是一个七元组(tr_id,source,target,cond,effect,prty,rv)；tr_id是迁移标识符；source和target分别表示迁移的源状态和目标状态；cond是关于全局系统状态的一个布尔条件；effect函数作用于全局系统状态，它可以修改全局系统状态；prty表示迁移的优先级，PROMELA中迁移的优先级由unless结构定义； rv表示迁移是同步通信(Rendezvous Channel)的接收消息操作。
定义6： System State（全局系统状态）
全局系统状态是元组(gvars,procs,chans,exclusive,handshake,timeout,else,stutter)；gvars表示全局变量有限集；procs表示进程的有限集；chans表示消息通道的有限集；exclusive默认值为0， 当atomic序列中的迁移执行时，会置exclusive为p.pid；handshake标志当前系统状态下有无同步通信发生；布尔变量timeout提供了从系统阻塞状态跳离的方法，仅当所有活动进程中没有可执行迁移时它为true，否则它一直为false；布尔变量else当且仅当当前进程局部状态下进程中没有可执行性迁移时为true；stutter是布尔值，用来确定stutter规则是否起作用；在初始系统状态，所有的进程位于其初始状态，所有的全局变量满足curval=inival；所有的消息通道满足contents={}，exclusive 和handshake为0，timeout、else和stutter初始值为false。
定义1到定义6给出了PROMELA语言中抽象对象的形式化定义，这些抽象对象的关系如图1所示。
2.2 PROMELA语句到语义模型的映射算法
下面我们探讨具体的算法。
第一步：我们考察在系统状态为s时，如何形成关于s的所有状态空间。令元组(p,t)表示对应于系统状态s时p进程及p中的一条可执行迁移t；集合E为二元组(p,t)的集合，它表示在系统状态s下的所有活动进程的所有可能迁移，即求得在系统状态s下的所有可能迁移状态。算法executable( State s)输入给定系统状态 和所有活动进程，输出集合E。executable(s)算法如下所示。
1 executable(State s)
2 {new Set E //创建关于元组(p,t)的集合E
3new Set e //创建关于元组(p,t)的集合e，中间变量
4E = {}
5timeout = false
6AllProcs:
7for each active process p
8 { if (exclusive == 0 //表示当前系统没有迁移处于atomic序列
9 orexclusive == p.pid) //检查进程p中atomic序列中的语句正在执行
10 { for u from high to low // 依P中迁移t优先级从高到低进行
11 { e = {};else = false
12 OneProc: for each transition t in p.trans
13 {if (t.source == p.curstate
14andt.prty == u
15andeval(t.cond) == true
16and(handshake == 0
17or handshake == t.rv) )
18{ add (p,t) to set e }
19}
20if (e != {}) //进程P中当前优先级下有可执行迁移
21{ add all elements of e to E //将可执行迁移t加入到E中
22break //结束优先级检查循环
23}
24else if (else == false) //进程P中当前优先级下无可执行迁移
25 { else = true //置else为true
26 goto OneProc //重新对p中迁移进行可执行性检查
27 }
28}
29}
30 }
31if (E == {} and exclusive != 0) //表示atomic序列中迁移已经执行完毕
32{ exclusive = 0 //重置exclusive为0并重新检查所有活动进程
33goto AllProcs
34}
35if (E == {} and timeout == false) //系统中无可执行迁移，重新进行选择
36{ timeout = true
37goto AllProcs //重新检查所有活动进程
38}
39return E //返回关于系统状态s的所有可能执行迁移(p,t)
40 }
进程p中atomic序列中的迁移执行时，算法置系统变量exclusive为p.pid。在算法executable(s)中atomic序列是如下处理的：算法首先测试系统变量exclusive的值（算法第8、9行）以确保atomic序列中的迁移执行不被中断，然后再执行其它测试。当atomic序列中的所有迁移都执行完毕后，应重置系统变量exclusive并检查所有活动进程（算法第32、33行）。
第二步：我们考察PROMELA语义引擎随机挑选路径对全局系统状态s影响。只要集合E不空，我们在E中随机选择一个二元组(p,t)并执行元组中的可执行迁移t，于是全局系统状态会迁移到新状态s'，t所属进程p的局部状态也会发生迁移；当集合E为空，系统停止运行。特别的，对应于S=S0，系统处于初始状态，所有的进程Pi(i≥0)也处于初始状态。
3 结束语
本文描述了PROMELA语法元素对应的语义模型，并通过算法描述了PROMELA随机交叉执行方式的工作原理。算法的关键是处理PROMELA中atomic序列和同步通信问题，即通过对PROMELA语义模型中的handshake处理，实现将同步通信的发送消息操作和接受消息操作看作一个完整的动作。通过对exclusive的处理，实现atomic序列的执行不会被其它语句随机交叉。理解PROMELA语义引擎的工作原理，将有助于我们理解模型检查工具SPIN是如何对分布式并发系统进行建模和验证的。
参考文献：
[1] Ben-ari M.Principles of the Spin Model Checker[M].London:Springer-Verlag,2008.
[2] Baier C,Katoen J.Principles of Model Checking[M].London,England:The MIT Press,2008.
[3] Holzmann,J G.Spin Model Checker:Primer and Reference Manual[M].Addison-Wesley Professional:2003.
[4] 黎升洪,缪淮扣.时态逻辑描述能力比较研究[J].计算机工程与应用,2006(22).