目录
1 引言 ........................................................................................................................................ 1
2 CPN 建模语言 ........................................................................................................................ 3
2.1 网结构、声明、标注.................................................................................................3
2.2 变迁的使能与发生 .....................................................................................................6
2.3 步骤、并发和冲突 .....................................................................................................9
2.4 模块 ........................................................................................................................... 11
2.5 时间建模 ................................................................................................................... 15
3 CPN 模型的构建 .................................................................................................................. 20
3.1 GUI 概述 ....................................................................................................................20
3.2 模型元素的构建.......................................................................................................21
3.3 层次模型构建 ...........................................................................................................23
3.4 语法检查和代码生成...............................................................................................25
3.5 图形化反馈与帮助 ...................................................................................................25
4 模拟 ...................................................................................................................................... 26
5. 状态空间分析 ..................................................................................................................... 30
5.1 为状态空间分析改进模型.......................................................................................30
5.2 完全状态空间 ...........................................................................................................31
5.3 状态空间报告 ...........................................................................................................33
5.4 查询函数 ................................................................................................................... 37
6 性能分析 .............................................................................................................................. 38
6.1 性能分析的赋时模型...............................................................................................38
6.2 性能测量和数据收集...............................................................................................40
6.3 统计 ........................................................................................................................... 42
6.4 性能输出 ................................................................................................................... 44
6.5 进行模拟实验 ...........................................................................................................46
6.6 模型参数及对比配置...............................................................................................47
7 可视化 .................................................................................................................................. 47
7.1 消息序列图............................................................................................................... 48
7.2 交互图形 ................................................................................................................... 49
8 结论 ...................................................................................................................................... 50
鸣谢 .......................................................................................................................................... 51
参考文献 .................................................................................................................................. 51
1
用于并发系统建模和验证的
着色 Petri 网及其工具软件 CPN Tools
Kurt Jensen, Lars Michael Kristensen, Lisa Wells
Department of Computer Science
University of Aarhus
IT-Parken, Aabogade 34, DK-8200 Aarhus N, DENMARK
e-mail: {kjensen,lmkristensen,wells}@daimi.au.dk
摘要:着色Petri网(CPNs)是一个用于建模和验证系统的语言,在这些系统中并发性、交互性
和同步性扮演着主要角色。着色Petri网是一种把Petri网与功能编程语言Standard ML结合起来的
离散事件建模语言。Petri网为建模提供图形注释以及并发性、交互性、和同步性的基本的原语基
础。Standard ML为数据类型定义、数据操作描述、创建紧凑的可参数化的模型提供基本原语。
一个系统的CPN模型是一个代表着系统状态和事件(变迁)的可执行模型,事件可导致系统改变
状态。CPN语言使一组模块来构件一个模型成为可能,这里面包括一种时间概念,这种时间概念
又使在被建模的系统中,表示处理事件所花费的时间成为可能。
CPN Tools,是一个为构建和分析CPN模型的工业价值的计算机工具。使用CPN Tools,可以
实现用模拟的方法调查被建模的系统的行为,借助状态空间方法和模型检查来验证性能,进行基
于模拟的性能分析。用户与CPN Tools交互,是基于对采用交互技术的图形表示的CPN模型的直
接操纵,如工具面板和(状态)标记菜单。工具的功能可以通过用户定义的Standard ML功能来
扩展。 CPN Tools的许可证可以免费得到,也用于商业用途。
关键词:着色Petri网,行为建模,确认,模拟,验证,状态空间方法,模型检查,性能分析,可
视化。
1 引言
系统工程是一门综合性学科,涉及各式各样的活动,例如需求工程、设计、规范化、实现、
测试与部署。开发分布式系统是特别具有挑战性的,主要原因是这些系统具备并发性和非确定性,
即此种系统的执行有许多不同的方式。这是极其容易使设计师在设计这种系统时错过一些重要的
交互模式,并导致在系统设计中出现功能偏差或错误。为了应对现代并行系统复杂性,提供能在
实现和部署之前,进行系统设计中中央部分的调试和测试的方法至关重要。
其中一个开发并行系统的富有挑战性的方法,就是要建立一个可执行的系统模型。构建模型
并模拟,通常可以使一些新见解被纳入系统设计和运行中,而且往往会导致一个更简单和更精简
的设计的产生。此外,构建一个可执行的模型通常会产生一个更完整的系统规范,便于场景的系
统化调查,这可显著降低设计中错误的数量。
着色Petri网(CP-nets或CPNs)[16,17,19,24] 是一种图形语言,用于为并发系统构建
模型,并分析其性能。CP-nets 是一个与Petri网[30]结合的离散事件建模语言,其功能性编程语
言CPN ML是基于Standard ML [33,34]的。CPN建模语言是一种通用建模语言,即它不是着重于
为特殊类型系统建模,而是旨在实现一个广泛类型的并发系统的建模。典型的CP-nets应用领域
包括通信协议[5],数据网[4],分布式算法[31],及嵌入式系统。然而,CP-nets也适用于更广泛
地以并发性和交互性为主要特点的系统建模。这类系统的例子有商业流程与工作流建模〔36〕,
制造系统[11]和代理系统。在不同工业领域的CPN应用的例子可以通过[12] 得到。文献[19,25]
1
给出了实际使用CP-nets的入门性介绍。
一个系统的CPN模型阐述了系统的状态和导致系统改变状态的事件(变迁)。通过CPN模型
的模拟,可以研究系统的不同场景,并探讨系统的行为特性。通常情况下,模拟的目的是调试和
研究系统的设计问题。CP-nets可以被交互的或自动的模拟。交互式模拟类似与单步调试。它提
供了一种方式,以“单步通过”(walk through)CPN模型,调查不同的场景并且检查模型是否
达到预期的效果。在一个交互的模拟过程中,建模人员通过在当前状态下使能的事件中做出选择
控制,并决定下一步该怎么做。可以在图形上直接观察CPN模型的单步运行效果。自动模拟则类
似于程序执行。目的是为了尽可能快地对模型进行模拟,其典型应用就是对模型进行测试和性能
分析。为了测试,建模人员通常设立适当的断点和停止运行的条件。为了进行性能分析,模型需
要有数据收集器,来搜集与系统的性能有关的信息。
在大量的并行系统中时间起着着重要作用。有些系统的正确运作关键取决于某些活动所占用
的时间,而且不同的设计决策都对系统的性能产生重大的影响。CP-nets包括一个时间概念,使
之能够捕捉在系统中执行活动所花费的时间。该时间概念也意味着CP-nets,可用于为基于模拟
技术的性能分析,研究影响系统性能的度量指标,如系统中的延迟、吞吐量、和队列长度,也可
以用于实时系统建模和验证。
CPN模型可以构造一系列模块来处理大规格的系统规范。这些模块通过一套定义完善的接口
相互交互,并用类似编程的方法来进行组织。CP-nets的模块概念是基于一个分层结构机制,允
许每一个模块有子模块,而且可以用一组模块来组成新的模块。
可视化是一项技术,该技术利用高层次的图形来生动的刻画CPN模型的行为,而且它与模拟
CPN模型密切相关。一个可视化的重要的应用是,它允许用应用领域的概念展示设计思路和分析
结果。这一点在与一般对CP-nets不熟悉的人和同事讨论时尤为重要。在CPN模型的顶层增加特
定领域图形的方法有许多,可用于在应用领域内从理论上展示CPN模型的执行。其中一个例子是
利用消息序列图(时间序列图)[7]在通信协议的执行中显示交换消息。
CPN模型是形式化的-本质上来说,CPN建模语言中有其语法和语义的数学定义。这意味着他
们可以用来验证系统特性,即证明某些需要的属性可以达到,或某些不需要的属性保证不会出现。
检查系统的特性是由一系列状态空间方法支持的。基础状态空间的基本思路是计算所有可能达到
的状态和有关CPN模型状态的变化,并以一个有向图表示这些变化,图中节点代表的状态,弧代
表发生的事件。状态空间可以完全自动构造。通过一个构造的状态空间回答一个系列与系统行为
有关的检查问题是有可能的,如有无死锁。即是否总是可以达到某种给定的状态,并保证提供某
项服务的可能性。CP-nets的状态空间方法也可应用于赋时的CP-nets。因此,它也可以通过赋时
CP-nets建模来验证系统功能的正确性。
应该强调指出的,为CP-nets以及他们支持的计算机工具的实际使用,需要对CPN建模语言
的语法和语义有一个直观的了解,这有点类似于普通的编程语言,如JAVA,可以被不熟悉这种
语言的形式化定义的编程人员所成功的应用。这里强调了一个重要的特性,那就是CP-nets可以
不用研究相关的正式定义就可以被教授和学习。
CPN建模和分析的实际应用,必须依赖于支持创建并操作模型的电脑辅助工具的存在。CPN
Tools[10]是一个关于CPN模型的编辑、模拟、状态空间分析和特性分析的工具套件。它是现在在
100多个不同的国家有4000多个经过许可的用户,并可用于MS Windows和Linux操作系统。CPN
Tools的用户直接工作于图形表示的CPN模型。CPN Tools的图形用户界面(GUI)没有传统菜单
栏和下拉式菜单,但是基于交互技术,如工具面板(tool palettes)和状态菜单(marking menus)。
CPN Tools的许可证可通过CPN Tools的网页免费获得[10]。
本文简要介绍了CPN建模语言和如何使用CPN Tools中支持的构建、模拟、状态空间分析、
性能分析,和可视化的说明。第2节介绍CPN建模语言的概念。第3节说明如何建造CPN Tools支
持的CPN模型。第4节显示模拟是如何被支持的。第5节给出了状态空间方法的简要的介绍,并说
2
明了他们在CPN Tools中是如何被支持的。第6节介绍了基于模拟的性能分析的基本思想,并说明
它是如何被CPN Tools支持的。第7节说明CPN Tools是如何支持领域可视化的。最后,第8节总
结本文并提供参考文献,以进一步对CPN建模语言、实例分析、和CPN Tools的使用进行学习。
读者指南
没有必要阅读完整篇文章或熟悉Standard ML后才开始使用CP-nets和CPN Tools。如果只是
了解基本内容,阅读以下的内容就足够了:CP-nets的非层次概念的介绍(Sects. 2.1-2.3),CPN
Tools和构造非等级模型的工具的介绍(Sects. 3.1-3.2 and 3.4-3.5),如何模拟CP-nets模型(Sect.
4)。关于CPN ML的基本介绍和一些实例,以及如何使用CPN ML,都可以在CPN Tools的帮助页
面查找(也可以通过网上查找[10])。
对于熟悉基本的CP-nets和CPN Tools的读者,文章中其余的章节的是目前较高级的课题。分
层的CP-nets在2.4节中介绍。以及构建层次模型工具在3.3节介绍。如果读者对性能分析感兴趣,
就应该阅读关于赋时的CP-nets的介绍(第2.5节)。第6节是关于性能分析的。状态空间分析和
可视化分别在第5节和第7节中介绍。不需要为了使用性能、状态空间和可视化设备的基本特征
而对Standard ML有一个良好的认识。但是,要想对这些设施更先进的功能进行有效的使用,就
必须要了解Standard ML。又比如,帮助页面提供了相当多的例子,并且说明了Standard ML是
如何被用于支持高级分析技术。
2 CPN 建模语言
在本节中我们通过一个小例子介绍了CPN建模语言,模型是对通信协议的建模。我们使用一
个简单的协议,因为它容易解释和理解,而且因为它涉及到并发性、不确定性、通信和同步,这
是并发系统的关键特点。协议本身不复杂,但对于说明CPN模型语言的构建是足够的。读者不需
要对协议的相关知识有一定的基础。
简单的协议包括一个发送器(sender),传输若干的数据包(data packets)到一个接收器
(receiver)。通信发生在一个不可靠的网络,即数据包可能会丢失而且超越也是可能的。协议
利用序列号、确认和重传技术以确保数据包被准确传输,并且没有重复传输,而且在传输结束后
数据包的顺序是正确的。该协议使用“停止-并-等待”策略,即,相同的数据包的传输直到收到
相应确认。被传输的数据包中包括一个序列号及数据(有效载荷)。确认包括一个序列号,用于
指明接收器期望的下一个数据包的编号。
2.1 网结构、声明、标注
一个CPN模型通常是像绘制图形一样被创建出来,图1展示了协议的基本CPN模型。左面的
部分为发送器建模,中间部分为网络建模,右边的部分为接收器建模。该CPN模型包含了8个库
所(places)(形状和圆一样),5个变迁(transitions)(形状为矩形盒),还有一些直接连接
库所和变迁的弧(arcs),最后是一些靠近库所、变迁、弧的标注(inscriptions)。这些标注在
CPN ML编程语言中有记录,它是Standard ML语言的扩展。库所和变迁被称为节点(nodes)。
与直接弧一起,他们构成了网结构(net structure)。一个弧总是把一个库所连接到一个变迁或
把一个变迁连接到一个库所。在两个同类的节点间是不允许有弧的,即在两个库所间或两个变迁
间都不允许有弧。
建模系统的状态是由库所代表的。每个库所都可以被一个或一个以上令牌(tokens)标识,
而且每个令牌自身都附有一个数据值,这个数据值是所谓的令牌颜色(token colour)。在每一个
单独的库所里的令牌数量和令牌颜色合起来,构成了系统的状态(marking)。在一个特定库所
3
上的令牌数构成了那个库所的状态。按照惯例,我们在椭圆形内写库所的名字。这些名字本身没
有规范的意义-但他们对CPN模型的可读性具有重要实际意义(就像在传统的编程中使用助记符
一样)。发送器(Sender)的状态是由两个库所PacketsToSend和NextSend 建模的。接收器
(Receiver)的状态是由两个库所DataReceived和NextRec建模的,而网络的状态是由库所A、B、
C和D建模的。
在每一个库所附近,都有一个标注决定了在此库所的令牌允许使用的令牌颜色集(数据值)。
一个可能的令牌颜色集是由一个类型(如已知的编程语言的类型)指定的,它被称库所的颜色集。
按照惯例,颜色集是写在库所下面的。库所NextSend,NextRec,C和D有颜色集NO。在CPN Tools
中,颜色集是使用CPN ML关键字colset定义的,并且颜色集NO被定义和整数类型等价:
int:
colset NO = int;
这意味着在四个库所NextSend、NextRec、C和D将有一个整数作为他们的令牌颜色。颜色集NO
被用来为建模协议中的序列号。在工具中,整数类型的大小,将取决于编写这种工具的编程语言。
例如,在CPN Tools中int 类型是31位整数。库所DataReceived 的颜色集 DATA 被定义为包含
所有的文本内容的字符串。颜色集DATA是用来为数据包的有效载荷建模的。其余的3个库所有颜
色集NOxDATA,它定义为NO 的类型和DATA的积。该类型包含所有第一个要素是一个整数而且
第二个要素是一个文本串的两元组。元组用是逗号分割的列表加括号(和)书写的。颜色集
NOxDATA是用来为数据包建模的,这些数据包包括一些顺序号和一些数据。颜色集的定义如下:
colset DATA = string;
colset NOxDATA = product NO * DATA;
每一个库所旁边,我们看到另一个标注,该标注决定这个库所的初始状态(initial marking)。
最初的原始库所的状态,按照惯例都是写在库所的上面的。举例来说,在库所NextSend右上方
的标注标明库所的原始状态是由一个有带颜色(值)的1个令牌构成的。这表明,我们希望数据
包1作为第一个被传送的数据包。类似地,库所NextRec也有一个初始的状态,它包括一个带有
颜色1的单一令牌。这表明接收器最开始期望接受标号为1 的数据包。库所DataReceived 有一
个初始的状态,这个状态包括一个带有颜色””牌(这是空的文本串)。这标志着该接收器还没有
4
开始接受任何数据。在库所PacketsToSend 左上方的Allpackets标注是一个常量,定义为:
val AllPackets = 1’(1,"COL") ++ 1’(2,"OUR") ++
1’(3,"ED ") ++ 1’(4,"PET") ++
1’(5,"RI ") ++ 1’(6,"NET");
这里指明,这个库所的初始状态有以下数据值的令牌:
(1,"COL"),(2,"OUR"),(3,"ED "),(4,"PET"),(5,"RI "),(6,"NET")。
该++与’运算符,这允许构成包括令牌颜色的多态集。多态集类似于集合,只不过值可以出
现不止一次。该中缀运算符' 左边要求正整数以指明右边的参数提供的元素出现的次数。该++
需要两个多态集作为参数,并且返回他们的并集(和)。PacketsToSend的最初状态有6个令牌,
代表我们希望传送的数据包。没有标注指明的初始状态意味着库所最初没有令牌。库所A,B,C,
D的就是这种情况。
每一个库所的当前状态(current marking)都紧靠库所。在当前状态中库所上令牌的数量都
在小圆圈中显示出来了。在最初时,当前状态等价于初始状态,表示为M0。就像前面解释的,
初始状态在PacketsToSend上有6个令牌,而且在库所NextSend、NextRec和 DataReceived每个
上有一个令牌。
5个变迁代表可以在系统中发生的事件。如库所一样,我们在长方形里写下变迁的名字。变
迁的名字也没有规范的含义,但他们对该模型的可读性都非常重要。当一个变迁发生(occurs)
时,它从其输入库所(input places)(那些有指向变迁的弧的库所)中去除令牌,而且它向其输
出库所(output places)(那些有一个来自变迁的弧的库所)中增加令牌。当变迁发生时从输入
库所移走,到输出库所增加的令牌的颜色值由弧表达式(arc expressions)决定。这些弧表达式
就是靠近单个弧的文本标注。一个变迁和库所之间也可以用双箭头弧(double-headed arcs)连接。
双箭头弧的是两个在一个库所和和一个变迁之间的相反的方向有向弧的简记形式,并且该库所和
变迁之间的弧有相同的弧表达式。这意味着库所对于变迁来说,既是输入弧也是输出弧。变迁
SendPacket和库所PacketsToSend和NextSend都通过双箭头弧连接。
弧表达式可以在CPN ML编程语言里写出,并从确定类型的变量、常量、运算符和函数构建。
当在一个表达式中的所有变量可以给定值时(正确类型的),表达式的值可以计算出来。一个弧
表达式可以由一个令牌颜色的多态集赋值。作为一个例子,考虑连接在变迁SendPacket 上的3
个弧上的2个弧表达式:n和(n,d)。他们包含的变量n和d的声明如下:
var n : NO;
var d : DATA;
这意味着n必须捆绑到一个NO类型的值上(即一个整数),而d必须绑定到DATA类型的值上
(即一个文本串)。例如,我们考虑绑定:
把n赋值为3,d赋值为“CPN”。这样把弧表达式赋成下面的数值,这里“→”应该被理解为“值
为”:
n → 1’3
(n,d) → 1’(3,"CPN")
弧表达式赋值为令牌颜色的多态集,这意味着有可能没有或者只有一个或者一个以上的令牌
被从输入库所中删除或是被添加到一个输出库所里。如果一个弧表达式值为一个令牌,那么这个
1 ' ,通常来说可从表达式中略去。举例来说,弧表达式n和(n,d)项的就是1' n 和1 '(n,d)
的简记形式。
5
2.2 变迁的使能与发生
下面我们考虑一下在一个CPN模型中事件的发生。在一个变迁的输入弧(input arcs)(那些
从一个库所到一个变迁的弧)上的弧表达式,与输入库所上的令牌一起决定该变迁是否使能
(enabled),即能在一个给定的状态中发生。为了使一个变迁使能,它就必须找到一个出现在
变迁周围的弧表达式的变量绑定,使得每一个输入弧的弧表达式是一个可求的值的对应于输入库
所的令牌颜色的多态集。当一个给定绑定的变迁发生时,它将从每个输入库所中移走对应输入弧
指定的令牌颜色的多态集。类似地,它增加到每个输出弧(output arc)上对应输出弧上指定的
令牌颜色的多态集。
现在我们考虑一下变迁SendPacket。在图1中,变迁SendPacket有一个厚厚的边界线,而其
他四个变迁没有。在CPN Tools,这表明SendPacket是在状态 M0中唯一一个有使能绑定的变迁。
其他变迁禁止,即他们不能发生。当这个变迁发生时,它可以从每一个输入库所NextSend和
PacketsToSend中去掉一个令牌。这两个双箭头的弧的弧表达式是n和(n,d)。
库所NextSend最初的状态包含一个单独的令牌与颜色1 。这意味着,该变量n必须绑定为1 。
否则,来自NextSend的弧上的表达式将得到一个不出现在NextSend中的令牌颜色,这意味着变
迁对于那个绑定来说是禁用。现在让我们考虑来自PacketsToSend的弧表达式(n,d)。我们已
将n绑定为1 ,现在看一下d的绑定,使得弧表达式(n,d)绑定为这6个令牌颜色中的一个,并
且这个令牌颜色出现在PacketsToSend上。很明显,唯一的可能是,把d的赋值为字符串"COL"。
因此,我们推测绑定:
是SendPacket唯一的使能绑定(在初始状态)。带有这个绑定的SendPacket的发生将从输入库
所NextSend中删除颜色为1的令牌,并且从输入库所PacketsToSend 中删除带有颜色(1,“COL”)
的令牌。因为SendPacket是通过双向弧与PacketsToSend和NextSend连接的,带有这些绑定的
SendPacket的发生也将添加一个颜色为(1,“COL”)的令牌到PacketsToSend中,同时增添
一个颜色为1的令牌到NextSend 中。这意味着根据弧表达式的结果,从库所PacketsToSend 和
NextSend中删除的令牌数,立即就被新增的同样颜色的令牌数代替了。因此当变迁发生时,这
些库所的状态并没有改变。这就允许数据包被重新发送(从数据丢失中恢复)。SendPacket的
发生也给输出库所A 增加了一个新的颜色为(1,“COL”)的令牌。直观来看,这代表了第一
6
个数据包(1 ,"COL" ),已经被送往网络。图2展示了在新状态 M1中的CPN模型的片段。我
们只是展示了CPN模型的片段,主要因为一个变迁的发生,只有与之连接的库所状态会发生改变。
考虑有3个变量n,d和success的状态 M1和变迁TransmitPacket。变量success是一个布尔变
量声明为:
var success : BOOL;
这出现在输出弧上。颜色集BOOL被定义为布尔值的集合({true, false})
bool:
colset BOOL = bool;
在状态 M1 中,库所A 有一个颜色为(1 ,"COL")的令牌。变量success仅在从TransmitPacket
的输出弧上找到。这意味着变量可以被赋值为是一个它的颜色集(这是BOOL类型的)中的任意
值。因为来自A的输入弧的弧表达式为(n,d),可以直接推论出,变迁TransmitPacket可以在
在M1的两个不同绑定使能,
bsucc =
bfail =
这些绑定中的第一个-bsucc,代表网上的传递成功。如果在M1中它发生,这时将会出现:
-数据包(1,"COL")被从输入库所A中去掉
-一个代表相同数据包的新的令牌被添加到输出库所 B中(在if-then-else表达式中,条件
success的值为true,此时1'(n,d)的值为1'(1,"COL"))。
,这是在M1中的绑定bsucc的发生的结果。
图3显示部分的状态
第二个绑定bfail代表一个不成功的传递,即该数据包在网络中被丢失。如果它发生在M1,以
下情况将出现:
-数据包(1 ,"COL")被从输入库所A中删除。
-没有令牌被添加到输出库所B中(在if-then-else表达式中,条件success的值为false,前面
定义的常量empty 的值为 empty 多态集)。
在M1中的绑定 bfail的发生将导致回到图1所示的初始状态 M0。
现在,让我们考虑在状态
中数据包的接收。在库所NextRec上的令牌,代表接收器期
待收到的下一个数据包的序列号。变量k是就赋值为这个序列号的数值。变量data有DATA数据类
7