（计算机软件与理论专业论文）基于petri网的软件模型验证.pdf

摘要 随着软件在人们生活中起着越来越重要的作用，如何提高软件的质量，保证 软件的可靠性和安全性成为一个重要的问题。在软件设计领域，u m l 成为广泛 运用的软件建模工具，但是u m l 作为一种半形式化语言，缺乏精确的描述和形 式化定义，很难验证模型的正确性。p e t r i 网既是一种图形化建模工具，又是具 有严格的语法语义定义的形式化方法，不但能有效地对系统进行描述和建模，对 系统的并发性、异步性和不确定性也有很强的动态分析能力。通过将u m l 模型 转化为p e t r i 网模型，再利用p e t r i 网的分析验证技术，可以实现对软件模型的正 确性的验证，在设计阶段即发现系统的缺陷，从而减少软件开发后期才发现设计 的错误而带来的损失，提高系统的正确性和安全性。 本文提出一种系统层次上的对u m l 状态图进行验证的方法，将u m l 状态 图转换为系统层上的p e t r i 网，然后使用模型检测的方法验证u m l 状态图转换 得到的p e t r i 网模型。并且通过验证状态图转换得到的p e t r i 网模型是否满足协作 图描述的用例而验证协作图，从而验证系统的动态行为。 本文通过将u m l 模型的x m i 格式进行解析，使用d o ma p i 实现了u m l 模型向p e t r i 网标识语言p n m l 自动转换。p n m l 可以被p e t r i 网建模工具c p n t o o l s 识别，从而对转换得到的p e t r i 网模型进行分析和模型验证。c p nt o o l s 提 供了一个可视化的界面，可以对p e t r i 网模型进行编辑和仿真，同时也可以验证 模型是否满足a s k - c r l 公式描述的性质。 最后，本文通过实例测试了在b o r l a n d t o g e t h e r ，c p n t o o l s 等环境下的转换 过程和验证了实现的系统的正确性。实现了u m l 建模过程和转换后的模型的自 动化验证过程的集成。 关键词软件建模，形式化方法，模型检测，u m l 模型，p e t r i 网 a ss o f t w a r ei sb e c o m i n gm 0 他a n dm o r ei m p o r t a n tt op e o p l e sl i f e h o wt oe n s u r e r e l i a b i l i t ya n ds e c u r i t yo fs o f t w a r et oi m p r o v et h eq u a l i t yb e c o m e sa nu r g e n ti s s u e a l t h o u g hu m l i sw i d e l yu s e da sam o d e l i n gt o o li ns o f t w a r ed e s i g nf i e l d s ，a sa s e m i f o r m a ll a n g u a g e ，i tl a c k sa c c u r a t ed e s c r i p t i o na n df o r m a ld e f i n i t i o n s ，w h i c hi s h a r dt ov e r i f yt h ec o r r e c t n e s so fm o d e l p e t r in e ti sn o to n l yag r a p h i c a lm o d e l i n gt o o l b u ta l s oaf o r m a lm e t h o dw i t hs t r i c tg r a m m a ra n ds e m a n t i cd e f i n i t i o n s p e t r in e tc a n b eu s e dt om o d e la n dd e s c r i b et h es y s t e me f f e c t i v e l y , a tt h es a m et i m e ；i th a ss t r o n g c a p a b i l i t yo fd y n a m i c a l l ya n a l y z i n gc o n c u r r e n c y , a s y n c h r o n ya n du n c e r t a i n t yo ft h e s y s t e m t h i sp a p e rp r e s e n t sa na p p r o a c ht ov e r i f yu m ls t a t ec h a r t sf r o ms y s t e ml e v e l f i r s ti tt r a n s f o r m su m ls t a t ec h a r tt op e t r in e ta ts y s t e ml e v e l ，a n dt h e nm o d e lc h e c k s t h ep e t r in e tm o d e l t h ea p p r o a c hv e r i f i e st h ed y n a m i cb e h a v i o ro fs y s t e mb y v e i l f y i n gw h e t h e rt h ep e t r in e tm o d e ls a t i s f i e st h eu s ec a s ed e s c r i b e db yc o l l a b o r a t i o n d i a g r a m t h i sp a p e rd e s i g n sa n di m p l e m e n t sa na u t o m a t i ct r a n s f o r mt o o lf r o mu m lm o d e l t op e t r in e t i tp a r s e st h ex m id o c u m e n to fu m lt oo b t a i nt h ei n f o r m a t i o no fu m l m o d e l a c c o r d i n gt ot h et r a n s f o r mr u l e s ，t h et o o li n v o k e sd o ma p it oi m p l e m e n tt h e a u t o m a t i ct r a n s f o r m a t i o nf r o mu m lm o d e lt op e t r in e tm a r k u pl a n g u a g e ( p n m l ) p n m lc a nb er e c o g n i z e db yap e t r in e tm o d e l i n gt o o lc a l l e dc p nt o o l s c p nt o o l s c a ne d i t ，a n a l y z ea n dv e r i f yp e mn e t sw i t hv i s u a li n t e r f a c e i tc a nb eu s e dt oa n a l y z e ， s i m u l a t ep e t r in e tm o d e la n dv e r i f yw h e t h e rt h em o d e ls a t i s f i e st h ep r o p e r t i e s d e s c r i b e db ya s k - c t lf o r m u l a i nt h ee n d ，t h i sp a p e rt e s t st h et r a n s f o r mp r o c e s su s i n gb o r l a n dt o g e t h e ra n dc p n t o o l s ，a n di tv e r i f i e st h ec o r r e c t n e s so ft h es y s t e mt h r o u g ha ni n s t a n c e t h ea p p r o a c h p r e s e n t e di n t h i sp a p e ri n t e g r a t e s t h eu m lm o d e l i n gp r o c e s sa n da u t o m a t i c v e r i f i c a t i o np r o c e s so ft h et r a n s f o r m e dm o d e l k e y w o r d s ：s o f t w a r em o d e l i n g , f o r m a lm e t h o d s ，m o d e lc h e c k i n g , u m l , p e t r in e t 学位论文独创性声明 本人所呈交的学位论文是我在导师的指导下进行的研究工作及 取得的研究成果据我所知，除文中已经注明引用的内容外，本论文 不包含其他个人已经发表或撰写过的研究成果对本文的研究做出重 要贡献的个人和集体，均已在文中作了明确说明并表示谢意 作者签名：至垒盔 学位论文授权使用声明 本人完全了解华东师范大学有关保留、使用学位论文的规定，学 校有权保留学位论文并向国家主管部门或其指定机构送交论文的电 子版和纸质版有权将学位论文用于非赢利目的的少量复制并允许论 文进入学校图书馆被查阅有权将学位论文的内容编入有关数据库进 行检索有权将学位论文的标题和摘要汇编出版保密的学位论文在 解密后适用本规定 学位论文作者签名：；厶炙 日期： 互4 ：! ：! 导师签名：泓l 毒 日期：笙2 ：! ：竺 基于p e t r i 网的软件模型验证 第一章引言 1 1 软件建模 第一章引言 模型是对现实存在的实体的抽象和简化。提供了系统的蓝图。模型过滤了非 本质的细节信息，抽象出问题本质，使问题更容易理解。为了建立复杂的软件系 统，我们必须抽象出系统的不同视图，使用精确的符号建立模型，验证这些模型 是否满足系统的需求，并逐渐添加细节信息把这些模型转变为实现。这样的一个 过程就是模型形成的过程，建模是捕捉系统本质的过程，也就是把问题从问题领 域转移到解决领域的过程。软件建模是开发优秀软件的一个核心工作，其目的是 把要设计的结构和系统的行为联系起来，并对系统的体系结构进行可视化和控 制。 现在的软件越来越大，大多数软件的功能都很复杂，使得软件开发变得更加 复杂和难以把握。解决这类复杂问题最有效的方法之一就是分层理论，即将复杂 问题分为多个问题逐一解决。软件模型就是对复杂问题进行分层，从而更好地解 决问题。这就是为什么要对软件进行建模的原因。有效的软件模型有利于分工与 专业化生产，从而节省生产成本。 使用模型便于从整体上、宏观上把握问题，可以加强人员之间的沟通，更早 的发现问题或疏漏的地方。模型为代码生成提供依据，允许我们详细说明系统的 结构或行为，给出了一个指导我们构造系统的模板，对我们做出的决策进行文档 化。 目前在软件刀：发过程中，u m l 作为一种通用的可视化建模语言被广泛使用。 u m l 提出了一套统一的标准建模符号，用于对软件进行描述、可视化处理、构 造和建立软件系统的文档。u m l 适用于各种软件开发方法、软件生命周期的各 个阶段、各种应用领域以及各种开发工具。u m l 能够描述系统的静态结构和动 态行为：静态结构定义了系统中重要对象的属性和操作以及这些对象之间的相互 关系；动态行为定义了对象的时间特性和对象为完成目标任务而相互进行通信的 机制。u m l 不是一种程序设计语言，但我们可以用代码生成器将u m l 模型转 换为多种程序设计语言代码，或使用反向生成器工具将程序源代码转换为u m l 模型，这也是o m g 组织正在力推的m d a 。除了u m l 之外，建模语言还新增 加了x m l 和m o f 。 1 2 形式化方法 形式化方法可以分为形式化描述和建立在形式化描述基础之上的形式化开 基于p e t r i 网的软件模型验证 第一章引言 发。形式化的描述就是用形式化的语言( 具有严格的语法语义定义的语言) 做描 述。形式化的软件开发，就是用形式化的语言来描述软件需求和特征，并且通过 推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。这样的验证 当然得建立在严格的语法语义的基础之上。在实际应用中，这是不容易做到的。 形式化方法研究的目的就是希望能够提供更好的理论、方法和工具，扩大形式化 方法的应用范围和使用价值。 形式化方法的意义在于它能帮助发现其它方法不容易发现的系统描述的不 一致，不明确或不完整，有助于增加软件开发人员对系统的理解，因此形式化方 法是提高软件系统，特别是s a f e t y c r i t i c a l 系统的安全性与可靠性的重要手段。最 早的形式化方法是逻辑与逻辑推理，它的目标是使推理机械化。从广义上讲，这 一目标受到许多挫折。比如说逻辑系统的不完备性( i n c o m p l e t e n e s s ) 、逻辑系统的 不可判定性( u n d e c i d a b i l i t y ) 、自动推理的难处理性( i n t r a c t a b i l i t y ) 。但是在一些实 际应用上，逻辑方法和自动推理还是起着非常大的作用。早期形式化方法在软件 验证的应用是串行程序的验证，后来随着软件研究和应用的发展，逐渐多样化 比如用逻辑和代数方法描述软件，用逻辑推理来验证软件( 即描述软件的这些逻 辑公式) 的性质。又比如用进程代数描述并发软件，用模型检测方法验证这些软 件的性质。近年来，由于认识到形式化方法重视的是严谨性，而这些方法与常用 的软件方法差别很大，逐渐有许多结合图形化软件方法、面向对象方法和形式化 方法的工作。以上所述几个方面( 即程序验证，定理证明，模型检测，图形化方 法和形式化方法相结合) 的内容虽然不尽一样，但密切相关。定理证明与模型检 测互为补充，各有所长。对于复杂的软件系统的验证，最好是能够结合多种方法 的使用。这些方法对高可信软件开发方法的探索和应用都极为重要。 形式化方法在软件开发中能够起到的作用是多方面的。首先是对软件需求的 描述。软件需求的描述是软件丌发的基础。例如一般非形式化的描述很可能导致 描述的不明确和不一致。如果描述的不明确和不一致导致设计，编程的错误，将 来的修改所要付出的代价非常大。如果导致的错误没有被发现，则影响程序的可 靠和使用。形式化方法则要求描述的明确性，而描述的不一致性也就相对易于发 现。其次是对软件设计的描述。软件设计的描述和软件需求的描述一样重要。形 式化方法的优点对于软件需求的描述同样适用于软件设计的描述。另外由于有了 软件需求的形式化描述，我们可以检验软件的设计是否满足软件的需求。对于编 程来讲，我们可以考虑自动代码生成。对于一些简单的系统，形式化的描述有可 能直接转换成可执行程序，这就简化了软件开发过程，节约了资源和减少了出错 的可能性。另外，形式化方法可以用于程序的验证，以保证程序的正确性。对于 测试- 束讲，形式化方法可用于测试用例的自动生成，这可以节约许多时间和在一 2 基于p c t r i 网的软件模型验证第一章引言 定程度上保证测试用例的覆盖率。 形式化方法原则上就是用数学与逻辑的方法描述和验证软件。从描述上讲， 一方面是系统或程序的描述，另一方面是性质的描述。这些可以用一种或多种语 言来描述。这些语言包括命题逻辑，一阶逻辑，高阶逻辑，代数，状态机，并发 状态机，自动机，计算树逻辑，线性时序逻辑，进程代数，丌演算，u 演算， 特殊的程序语言，以及程序语言的子集等。从验证来讲，主要有两类方法，一类 是以逻辑推理为基础，另一类则以穷尽搜索为基础。逻辑推理有n a t u r a ld e d u c t i o n ， s e q u e n tc a l c u l u s ，r e s o l u t i o n 以及h o a r e 1 0 9 i c 等方法。穷尽搜索方法统称为模型检 测。这类方法与系统或程序以及系统性质的表示有很大的关系，比如说符号模型 检测，其基本原理是用命题逻辑公式表示状态转换关系，用不动点算法计算状态 的可达性以及这些状态是否满足某些性质 形式化方法的应用在电路设计和协议设计上都取得了很大的成绩。但是对于 软件来讲还有很多没有解决的问题。软件的描述要比电路和协议复杂。一个软件 描述所包含的状态空问通常来讲可以是无限的。因此验证的难度很大。逻辑推理 的不足之处在于推理的难度。对于稍微复杂的系统，自动化的推理就难以胜任。 人为的推理有很大的缺点，除了费时费力外，比如说一个定理推不出来，并不能 说明这个定理不成立，很可能是推理方法和策略应用不当。模型检测的好处在于 它有全自动化的检测过程，并且如果一个性质不满足，它能给出这个性质不满足 的理由。我们即可据此对我们的系统描述进行改进。模型检测的困难首先是它所 能检测的是有限状态模型。这样对于一般软件来讲，需要有一个从任意状态到有 限状态的建模过程。并且这样的一个模型的状态空间会面临组合爆炸的问题。 1 3 研究意义 确保软件系统正确性和安全性的传统方法是对其进行反复测试即在系统建 立之后，利用所能够预想到的各种测试用例检测系统性能的正确性。然而，即使 系统能通过所有可以预想到的测试用例，但是仍然无法保证它对所有的实际情况 都能得出正确结果。因此，这就要求我们在系统开发过程中，能够利用形式化的 方法模拟系统的行为，并且验证它是否满足其规范说明 系统规范验证的方法是模拟所有可能的运行状态下系统所有可能的输入，因 此我们需要使用形式化方法模拟系统行为，使用逻辑语言表示系统的规范说明并 且需要一个有效的算法来验证所构建的系统模型是否满足用逻辑语言表述的规 范说明。 在软件设计领域，u m l 成为广泛运用的软件建模工具，但是u m l 作为一种 半形式化语言还没有有效的模型分析验证的方法。p e t r i 网既是一种图形化建模 基于p e t r i 网的软件模型验证 第一章引言 工具，又是具有严格的语法语义定义的形式化方法，不但能有效地对系统进行描 述和建模，对系统的并发性、异步性和不确定性也有很强的动态分析能力。通过 将u m l 模型转化为p e t r i 网模型，再利用p e t r i 网的分析验证技术，可以实现对 软件模型的正确性的验证，在设计阶段即发现系统的缺陷，从而减少软件开发后 期才发现设计的错误而带来的损失，提高系统的正确性和安全性。 1 4 本文的主要工作 1 ) 针对u m l 模型在软件建模领域广泛应用但是缺乏有效的模型验证方法 的情况，通过将u m l 模型转化为p e t r i 网模型，将软件模型的验证软换为p e t r i 网模型的验证，有利于将形式化技术应用于软件模型验证上。本文提出了一种在 系统层上将u m l 状态图转换为p e t r i 网的方法，并通过将u m l 模型导出为x m i 格式，利用d o m a p i 编写j a v a 程序来实现语义转换规则，实现了从u m l 状态 图向p e t r i 网自动转化。 2 ) 从u m l 模型转化得到的p e t r i 网可以被p c t r i 网建模工具c p nt o o l s 所 识别，并对p e t r i 模型进行仿真分析和模型检测，除了对原u m l 状态图进行模 型验证外，u m l 模型中的协作图也可以通过验证状态图转换得到的p e t r i 网模型 是否满足协作图描述的用例而得到验证。因此，u m l 模型的动态行为可以得到 验证。 3 ) 使用计算树逻辑作为系统规范的形式化描述。使得对系统需求的描述是 精确的，有利于验证系统模型满足规范说明，文章使用a s k - c t l 公式描述需要 验证的性质。 4 ) 通过实例对论文的方法进行实验，对实例进行u m l 建模，然后将u m l 自动转换为p e t r i 网模型，并对p e t r i 网模型进行了验证，验证了系统的动态行为。 1 5 本文的组织结构 本文的具体组织结构安排如下： 第2 章介绍了p e t r i 网的基本概念，包括语法、语义、性质等。 第3 章介绍分支时序逻辑中的计算树逻辑c t l 的语法、语义，并描述了对 c t l 公式描述的性质进行模型检测的过程。 第4 章首先描述了u m l 模型的组成，包括u m l 中的事物、关系和视图等。 然后详细描述了从u m l 模型到p e t r i 网模型的转化过程，提出了从系统层次上 将u m l 状态图转换为p e t r i 网的算法。最后给出了自动转换工具的设计和实现。 第5 章首先描述了p e t r i 网需要验证的性质，然后介绍了p e t r i 网模型验证算 法，最后描述了p e t f i 网模型的验证过程和使用的工具。 4 基于p e t r i 阿的软件模型验证第一章引言 第6 章中，通过具体的应用实例展示了从u m l 模型到p e t r i 网的转换过程， 并验证了所构建的模型是否满足时序逻辑所描述的形式化规范，最后验证了 u m l 协作图是否具有和状态图相一致的动态行为。 第7 章是对相关工作的介绍和本文研究工作的总结。 5 基于p e t r i 网的软件模型验证 第二章p e t r i 同 2 1 基本网 第二章p e t r i 网 p e t r i 网j i a 0 3 既是一种图形化建模工具，又是具有严格的语法语义定义的形 式化方法，能精确地描述系统之间的顺序、并发、同步等关系，适合描述复杂系 统的动态过程，并且有数学方法和工具对p e t r i 网模型进行检测和验证。 研究p e t r i 网系统模型行为特性包括：状态的可达( r e a c h a b i l i t y ) ，位置的有 界性( b o u n d e d n e s s ) ，变迁的活性( 1 i v e n e s s ) ，标识之间的可达( r e a c h a b i l i t y ) ， 变迁之间的一致性( p e r s i s t e n c e ) ，事件之间的同步距离( s y n c h r o n i cd i s t a n c e ) 和 公平性( f a i r n e s s ) 等。p e t r i 网模型的主要分析方法依赖于可达标识图与可覆盖 性树、关联矩阵和状态方程、不变量和分析化简原则。 从p e t r i 网的发展过程来看，它的纵向发展表现为：从条件事件网，经过库 所变迁网，发展到高级网。横向发展表现为：从无参数的网，发展到着色网、事 件p e t r i 网和随机p e t r i 网：一般有向弧发展到禁止弧和可变弧；从自然标记个数 到概率标记个数；从原子变迁发展到谓词变迁和子网变迁。 2 1 1p e t r i 网的结构 p e t r i 网是一种网状信息流模型，包括条件和事件两类结点，在条件( 称作库 所) 和事件( 称作变迁) 为结点的有向二分图基础上添加表示状态信息的令牌 ( t o k e n ) 分布，并按引发规则使得事件驱动状态演变，从而反映系统动态运行 过程。其形式化描述如下。 定义2 1 三元组n = ( p ，t ：f ) 称为网当且仅当； ( 1 ) p u t _ 中p n t - 中： 一( 2 ) f ( p x r ) u ( r x v ) ( 3 ) d o m ( f ) u c o d 【f ) 一p u t p 表示库所结点集合，t 表示变迁结点集合，f 称为流关系。p 中的元素称为 p 元素，t 中的元素称为t 元素。f 是由一个p 元素和一个t 元素组成的有序偶 的集合。d o m ( f ) 是有序偶的第一个元素的集合，c o d ( f ) 是第二个元素组成的集合。 即： d o m c f ) 一b l 方：0 ，) ，) ， c o d ( ，) 一矗1 3 y ：( ) ，工) f p u t 一垂，p n t - 西要求n 至少含有一个元素，且库所和变迁是不同的两 6 基于p c t d 网的软件模型验证 第二章p e t r i 孵 类元素，d o m ( f ) u c o d 陋) = p u t 要求n 不能有孤立元素，即p ，t 和f 均不能 为空集。 对v x e p u t ，令 k 一 y l ( y p u r ) ( ( y ，工) ，) 和，一 y i ( y e p u r ) ( ( 工，) ，) ，) ) 则称和矿分别为x 的前置集和后置集。 一个p e t f i 网p n 的结构可以用一个关联矩阵c 4 一门x n 表示。其中，m ：i p i ， = r r l ，并且 白。 1 ，p ie t j m - t j 一1 , p j ej t l t ； 0 。其他 定义2 2 四元组p n = ( p ，t ；f ，m o ) 称作p e t r i 网当且仅当 ( 1 ) n = ( p ，t ；f ) 是一个网； ( 2 ) m ：p z ( 非负整数集) 为标识( 也称状态) 函数，其中，m o 是初始 标识： ( 3 ) 引发规则： ( 3 1 ) 变迁f r 称为使能的当且仅当：v p ：肘( p ) 1 ，记f f - m t ，； ( 3 2 ) 在m 下是使能的变迁t 可以引发，引发后得到的后继标识肘， 则 m ( p ) 。 肘( p ) + l ，p f 。一| m ( p ) - l , v e v r m ( p ) ，其他 记作m 【i ，m 。 p n 的标识可以用一个非负整数的i n 维向量表示，记作m 。其中， m ( f ) 一肘b ) i - 1 , 2 - - , m 。 2 1 2 网的图形表示 p c t r i 网中，用线形的符号如方框或者竖线表示变迁结点，用圆形符号如圆圈 或椭圆表示库所结点，变迁结点之间、位置结点之间不能存在有向弧，变迁结点 与库所结点之日j 连接有向弧，网的某些库所标示若干托肯( t o k e n ) 。如图2 1 。 7 基于p e t r i 网的软件模型验证第二章p c t i i 同 图2 1p e t r i 网p n 在图2 1 中，p = p l ，p 2 ，p 3 ，p 4 p 5 ，t = t t ，t 2 ，t 3 ，t 4 ，t 5 ) ，f = ( p l ，t 1 ) ，( p 2 ， t 1 ) ，( t l ，p 3 ) ，( v 3 ，t 2 ) ，0 2 ，p 1 ) ，0 1 ，p 4 ) ，( v 4 ，t 3 ) ，0 3 ，p 5 ) ，( v 5 ，t a ) ，( p 5 ，i s ) ，0 4 ，p z ) ，( t 5 ， p 4 ) ，1 = p l ，p 2 ，p 妒= t 4 t 5 。 2 1 3 网系统 定义2 3 设n = ( p ，t ；f ) 为有向网。 ( 1 ) 若k 为从p 到z + u o 。，的映射，k ：p z + u p ，其中z + - - 1 ，2 ，3 ， 就说k 是n 上的一个容量函数。k ( p ) 一扣 表示p 的容量为无穷。 ( 2 ) 若k 是n 上的容量函数，m ：p z 。叫做n 的一个标识的充分必要条 件是：坳e p ：m 0 ) s k ( p ) ，其中z o = o uz + 。 ( 3 ) 映射一z + 称为n 的权函数，w 在弧( x ，y ) 上的值w ( x ，y ) 表示。 k m w 都可以在网上的图形中表示出来。k ( p ) 的值可以写在表示库所 的圆圈旁w ( x ，y ) 的值写在表示( x y ) 的弧上。容量表示每个库所存储资源 的最大数量，但不时当前的实际资源数。标识m ( p ) 代表库所中的资源数。对 网系统来说，同一库所中的所有资源都是完全等价的个体，所以可以用完全一样 的黑点来表示它们，将这个黑点称为托肯( t o k e n ) 。值为无穷的容量和值为1 的权一般都从图中略去。网的状态可以由标识的序列来确定。 定义2 4 六元组z = ( p ，t ；f ，k ，w ，m 。) 构成一个谓词，变迁( p t ) 系统的充 要条件是： ( 1 ) n - - ( p ，t ；f ) 是个网，称为三的基网， ( 2 ) k ，w ，m o 依次是n 上的容量函数，权函数和标识。m o 称为三的基本 标识。 网系统又称为被标识的p c 啊网。 定义2 5 令z 一( p t ；f ，k ，w ，m o ) 是一个p 厂r 系统。 ( 1 ) 函数：m ：p 一叫做z 的标识，当且仅当坳e p ：m 。0 ) s k ( p ) ； ( 2 ) 一个变迁t e t 在标识j l f 下是可实施的，当且仅当 _ e p ：w ，) s m 0 ) s k d ) 一矽( f ，p ) ； 8 基于p e t r i 网的软件模型验证 第二章p e t r i 网 ( 3 ) 如果t e t 在标识m 可实施，则实施t 后产生的新标识m 为： v p p , m ( p ) 一m ( p ) 一r y e , ，f ) + ( f ，p ) 。 系统标识m 经过t 的实施得到的新标识m 可以表示y g m t ，m 。 2 1 4 并发与冲突 定义2 6 设p e t r i 网p n = ( p ，t ；f ，m o ) ，m 是p n 的一个标识。若| f l ，t 2 e t ， 使得 m k ， 肘【f ：， 则当 ( 1 ) m t i m l - m l 【f 2 m 【f 2 m 2 _ m 2 【f l 时，称t l ，t 2 在m 下并发； t l 罟虽1 2 t l ( a ) 并发c o ) 冲突 图2 2 并发和冲突 ( 2 ) m t l m l _ 1 m 1 【f 2 i 肘【f 2 m 2 - 1 m 2 p l 时，称t l ，t 2 在m 下冲突。 定义2 7 设p e t r i 网p n = ( p t ；f ，m o ) ，m 是p n 的一个标识，若j 口r ， 嚣。沙撕印嚣则轴枷隈僦嘞叶并 2 1 5p e t r i 网的分析技术与基本性质 定义2 8 设p e t r i 网p n = ( p ，t f ，m o ) ，若埘1 ，m 2 ，m 。，使得： v 1 f 七，3 t f c t ： t p l m f + i 则称变迁序列盯。f 。t 2 厶在m l 下是使能的，m k + l 从m i 是可达的，记作 m l p m m 定义2 9 设p e t r i 网p n = ( p ，t ；f ，m o ) ，令r ( m o ) 为满足下列条件的 最小集合： ( 1 ) m o r o ) ； ( 2 ) 着m r 。) ，g t e t ，使得m p m ，则m t r 似o ) ； 则称r 似。) 为p e t r i 网p n 的可达标识集合。 定义2 1 0 设p e t r i 网p n = ( p ，t ；f ，m o ) ，若o e t , 埘郇似o ) ：m p ， 9 基于p e t r i 网的软件模型验证 第二章p e t r i 网 记撑( f ，盯l 为t 在o 中出现的个数。令 。x 0 ) 一撑e ，盯j ，礼2 ，厅 则称向量x 为引发数向量。 定义2 1 1 设p e t r i 网p n = ( p ，t ；f ，m o ) ，若m o m ，m ，m e r 似o l 盯r ， 则称m 一 f + c y 为p e t r i 网p n 的状态方程 定义2 1 2 称p e t r i 网p n = ( p ，t f ，m o ) 是活的当且仅当 v t e t ，v me r o l 埘t r ) 使得m i t 。 定义2 1 3 称p e t r i 网p n = ( p ，t ；f ，m o ) 是公平的当且仅当 v t l ，t 2e t ，孤 0 ，对v me r 似o l v o e t 都有 m a ， 撑纯a ) - 0 一群t j o ) k ，f ，乜2 f ， 定义2 1 4 称p e t r i 网p n = ( p ，t ；f ，m o ) 是有界的( 安全的) 当且仅当 v 肘e r o l 坳e p , 致之。使得肘( p ) 墨七( 七一1 ) 2 2 高级p e t r i 网 出于基本网模型不能反映时间方面的内容，并且模型容易变得庞大，不支持 构造大规模模型，为解决基本网的问题，对基本网进行了各种扩展，研究提出了 高级p e t r i 网，如着色p c t r i 网，时间p e t r i 网，面向对象的p e t r i 网等。 高级p e t r i 网的相对于基本网来说，允许建模者进行更简洁和可管理的描述， 同时又具有一般p e t r i 网的分析和验证的形式化方法，可以用来描述更大更复杂 的系统。一个复杂的模型可以通过网的结构、网的描述和声明来表示。允许我们 通过弧表达式来表示简单的数据操作，而不需要通过一些库所和变迁的繁琐组合 来表示这个简单的操作。在基本网中，仅有一类托肯，意味着库所的状念可以用 整数来描述。在高级p e t r i 网里，每个托肯可以携带一些复杂的信息，例如着色 p c t r i 网使用颜色来表达托肯所携带的信息。 2 2 1 着色p e t r i 网 着色p e t r i 网是一种高级p e t r i 网，在各个领域有着广泛的应用。着色p e t r i 网是p t 网模型的有用的约简。所谓约简，是指这两个网模型有共同的语义并且 该网的任意一个网都存在一个语义上与其等价的p 厂r 网( 一般更大) 。着色p e t r i 网这种约简的特征主要体现在：使用颜色来表达托肯所携带的信息以及可以借助 于变迁的不同发生实例来分解活动的能力。 在着色p e t r i 网中，托肯拥有多种颜色。托肯的颜色集可以是有限集也可以 是无限集。从系统工程的意义上考虑，一个可数的无限集作为托肯的颜色集也是 适合的。有限的颜色集可能限制较多，而不可数的颜色集又没有实用意义，他们 都可能妨碍性质的计算。 1 0 基于p e t r i 用的软件模型验证 第二章p e t r i 同 对于网中任何一个库所都规定一个允许的颜色集。如果某个变迁产生的托肯 的颜色在其后继的某一库所中不被接受。那么这个变迁不能被触发。 对于着色p e t r i 网的每一个变迁，其消耗的和产生的托肯的颜色之间都有一 个关系。这个关系通过前置条件和后置条件描述出来。如果一个变迁被触发，那 么一定有它的消耗的托肯满足前置条件，而产生的托肯满足后置条件。这些前置 条件和后置条件都通过弧上的表达式和变迁的断言来解释。 着色p e t r i 网的形式化描述如下： 定义2 1 5 设s 是个非空集合，n 是非负整数集，则从s 到n 的函数叫做s 上的多重集。s 的多重集m l s 一i ，非负整数肌g ) 是元素s 在多重集m 中出现的次数。通常用罗用g - 来表达多重集形式上的总和。s 。表示基于集合s 的所有多重集。非负整薮集钿g ) l s s l 称为多重集肌的系数，g ) 被称为元素s 的系数。一个元素s e s 当且仅当小g ) 一0 。空的多重集就是所有系数为0 的多重 集，用中表示。 定义2 1 6 多重集的运算 设m ，m l ，m 2 s m ，n e n ： ( 1 ) m 。+ 所：一罗。g ) + 研：g ) 必 ( 2 ) 雄m 。了筇删6 协 m 。一m ：一 s e s ：b 。g ) 一m ：g ) 】 。3 埘。g ) m ：g ) 一v s e s ：i r a 。g ) s 删：g ) 】 ( 4 ) h - 罗历0 ) 答 ( 5 ) 当s 脚：，m ：一m ，- ( m ：g ) 一m ，g 疆 着色p e t r i 网中，值和变i j e 酌出现方式的关联常表示为含有变量的表达式。 对每一个变迁定义一个变量的有限集合，此集合严格囿于此变迁。这些变量都有 类型或者颜色集，一般是与此变迁相连的库所的颜色集组成的集合。给变量赋值 称为绑定。在变迁上可以通过谓词来定义适当的约束，称为哨( g u a r d ) 。 变量v 的类型用日p e ( v ) 表示。 表达式e x p r 的类型用t y p e ( e x p r ) 表示。 表达式e x p r 中的变量集用v a r ( e x p f ) 表示，该变量集合只包括自由变量( 如表 达式中没有被内部绑定的变量) 。 一个集合变量的绑定y h ，v ：， 由。- c 。，y ：一c ：，吒一q ) 表示a 对 于每个变量q y ，c it y p e ( v i ) 。 求一个绑定中表达式的值由e x p r ( b ) 来表示。v a r ( e x p r ) 是b 中变量的一个子集， 求值通过用值c ；t y p e ( v ，) 替代每个变量h 砌r ( e x p r ) 来实现。 基于p c t i i 网的软件模型验证第二章p c t r i 网 定义2 1 7 着色p c t r i 网是一个多元组c p n 一侄，p ，t ，a ，n ，c ，g ，e ，i n ) ，其中： ( 1 ) 是一个类型( 称为颜色集) 的有限集合，每个颜色集是有限非空的 ( 2 ) p 是库所的有限集合。 ( 3 ) t 是变迁的有限集合。 ( 4 ) a 是弧的集合：p n t p n 彳一z n 彳一垂 ( 5 ) n 是一个结点的映射，从p 映射到p x t u t p 。 ( 6 ) c 是一个颜色的映射，从p 映射到。 ( 7 ) g 是一个守护函数，r ：b 弘( g ( f ) ) 一b o o l t y p e r ( g ( f ) ) ) 】。 ( 8 ) e 是一个弧表达式函数，它从爿映射到以下的表达式： v a c a ：d 功e 仁o ) ) 一c 0 q ) k t y p e 她r 仁0 ) ) ) z 】p ( 口) 是( 口) 的库所。 ( 9 ) n 是一个初始化函数，从p 映射到以下的表达式： v p e p ： t y p e 0 ) ) = c o , k t y p e 恤，0 ) ) ) 一中】。 颜色集的集合决定了类型，所有的颜色集是有限的。这个限制意味着一个函 数f 阻一j 到另一个函数f 口。一】的线性扩展总是收敛的。这样的 函数被用在库所不变量和变迁不变量里。 库所、变迁和弧由三个集合p ，t 和a 来表示，这三个集合是两两不相交的。 相对基本p e t r i 网而言，它允许网结构是空的。 结点函数把弧映射到一对序偶，第一个元素是源节点，第二个元素是目的节 点，这两个节点必须是不同类型的，如一个为库所，另一个为变迁。 颜色函数c 把每个库所p 映射到一个托肯颜色集c ( p ) ，每个库所p 上的托肯 必须有一个属于c ( p ) 类型的颜色。 守护函数g 映射每个变迁t 到一个值为布尔类型的表达式，也就是一个谓词， 而且，所有g ( t ) 中的变量必须含有属于中的类型。 弧表达式函数e 映射每条弧到一个表达式，这个表达式必须属于c ( p ( 口比类 型即基于c ( p ) 的多集。这意味着每个表达式的求值产生一个颜色集上的多集， 该颜色集是与相应的库所联系在一起的。我们也允许一个弧表达式是c ( p 0 ) ) 类 型的。在这种情况下，该弧表达式的值为一个属于c ( p ( 口) ) 的颜色值，我们认为 它是仅有一个元素的多集。 初始化函数玳映射每个库所p 到一个类型为c 0 ( 口比表达式一即一个基于 c ( p ) 的多集。这个表达式不允许含有任何变量。为了方便，也允许初始表达式 是c ( p ) 类型的。 令z p u r 表示所有的节点集，那么： j i 彳一xi 映射每条弧4 到它的源节点。 d k x l 映射每条弧口到它的目的节点。 基于p e t t i 网的软件模型验证第二章p e t r i 网 p 豳一p l 映射每条弧n 到q ) 中的库所。 f 阻一r 】映射每条弧n 到( 口) 中的变迁。 a e ( p x t u r p ) 一以】映射每个有序对到它们的连接弧，即该弧以并。为第 一个节点，以工：为第二个节点： 爿g 。，工：) 一矗爿l ( 口) 一g 。，工：) a e 防一x ，】映射每个节点到它周围的弧的集合，诸如那些为x 为源节点或 目的节点的弧： x g ) 一& t z i 勘爿：【0 ) 一g ，fv g ) 一g ，工珊 以上的函数通常都能扩展到以集合为输入，返回集合。 下面讨论着色p e t r i 网的动态行为。首先，定义一些表示符号： 用y a r ( t ) 表示t 的变量集，e g 。，x ：) 表示g 。，工：) 的表达式：