（计算机软件与理论专业论文）一类对象petri网建模与验证方法研究.pdf

内容摘要 一类对象p e 砸网建模与验证方法研究 内容摘要 p e 砸网是一种既有直观的图形表示方式，又有严格数学理论基础和多种分 析方法的建模工具。使用p e 砸网的分析方法可以刻画系统的结构，展现系统的 运行机制，表示和分析系统的动态行为。带有对象的p e 研网( p n o ) 是将面向对象 方法和谓词变迁网有机结合而定义的一种高级p e 砸网。因为p n o 在初始化和 验证具体系统时才构建库所的标识关系，变迁的使能与对象状态相关，并且变迁 的实施需要修改托肯和相关对象的属性，因此不便于直接使用常规的分析技术验 证p n o 模型。 针对p n o 模型存在的分析验证问题，本文将时态逻辑引入p n o 模型，提出 了相应的建模及验证方法。建模方法使用精确标识p n o 描述系统体系结构模型， 并通过时态逻辑定义模型上的需求和限制。验证方法使用s m v 工具验证p n o 模型和时态逻辑之间的一致性，该方法包括三个步骤。首先，根据s m v 的要求 在模型中增加与变迁有关的对象属性，并根据增加的对象属性细化变迁附加条件 函数和变迁实施处理函数。其次，使用时态逻辑公式描述系统的属性。最后，通 过算法p n 0 2 s m v 将p n o 模型转换成s m v 程序表示的有限变迁系统，以验证 有限变迁系统是否满足系统属性对应的逻辑公式，从而确保了系统设计的正确 性。 本文将上述建模及验证方法应用在列车运行模型( t o i p n o ) 上，通过在某一列 车运行区域和列车运行图实例上的应用表明：使用本文提出的建模及验证方法可 以在系统开发过程的更早阶段揭示潜在的问题，确保系统设计的正确性，从而实 现系统设计和分析验证之问的高度完整性。 关键字：带有对象的p e 城网，列车运行p n o 模型，s m v ，建模，验证 t 内容摘要一类对象p 靠i 网建模与验证方法研究 a b s t r a c t p e 砸n e t sa sam o d e l i i 培t o o lh a v et h ep r o p e n i e so f v i s u a l 口a p l l i c a lr 印r e s c n t a t i o 玛 s m c tm 址e 缸l a t i c a lm e o r y 龃dm 山t i p l ew o r k d b l e 缸a 1 ) r t i c a lt e c 眦q u e s u s i n gt h e s e a n a l y t i c a lt e 涮q u e s ，w ec a nd e s c r i b e 血es y s t 咖ss m l c t u r e ，r e v e a lt h es y s t e m s 叩e 豫t i 】唱m e c h a l l i 锄，i n d i c a t ea n d 卸a l y z em es y s t e m i sd y n a m i cb e h a v i o r s t h ep 酬 n e tw i t ho b j e c t s ( p n o ) i sak i n do fh i 曲一1 c v dp e 砸n e tw h i c hi n t e 斟a t e sm c o b j c c t 枷e n t e da p p r o a c ha n d1 l l ep r e d i c 鼬s i t i o nn e t s t h er d a t i o n s h i p sb c t w e e n p n o t sp l a c c sa r ec o n s 协l 曲e dw h e ni i l i d a l i z i i l ga n dv 甜劬n gap a n i c u l a rs y s t e m ， w t l i l om ee 1 1 a b l ec o n d i t i o i l so fa 蛔n s i d o na r ec o n c 帅e dw 浊s t a t e sa n dt u p l e so f o b j e c t s 锄dt h e 鼬i n go fa 妇l s i t i o n 晰l lm o d i 母t h ep r o p 训e so f t o k e na 1 1 dr e l a t c d o b j e c t s f o ra 1 1f e a 如r c sa b o v ei ti si m p o s s i b l et ov e r i 母t o p n ou s i n go r d i n a r y a i l a l y t i c a lt e c h l l i q u c sd i r e c t l y a i l l l i n ga t 曲ep r o b l 锄so f v e r i 蛳n gp n 0 ，t l l i sp 印e ri n 呐d u c e st e i n p o r a ll o 番ct o p n 0m o d e la n dp r e s e i l t sam o d d i n ga i l dv 嘶聊n gm e t t l o db a s e do np n o 、i m p r e c i s em a r k i n g t h em o d e l i n gm e t h o dd e f i n e sm ed e c i s i o n sa b o u “h ea r c h i t e c t u t eo f as o f t w a r es y s t e mw i t hp e 砸n c t s ，a 1 1 ds p e c 墒e st h er e q u i r e m 髓t sa n dc o n s t r a i n t s i m p o s e do n l es o r w a r ea f c l l i t e c t l l r 。w i t l lt 锄p o m ll o 百c t h ev e r i f m n gm e m o d v 酬6 e sm ec o n s i s t c n c yb 计吣e nt l l ep n o 锄dt l l et 锄p o r a l l o 百cf o 肿u l ab a s e do n s y m b 0 1m o d dc h e c k ( s m v ) 1 kv 谢助n gm e m o dc o n s i s t so f 恤e es t 印s t ob 哂n ， t h em c t h o de x t c n d st 1 1 ec l 船sp r o p e r t i e sr e l a c e dt ot l l em m s i t i o n ，a i l dr e f i n e st h ee x t m c o n d 谢o nf l m c t i o n sa 1 1 dm et r e a 咖e n t 如n c t i o n sa c c o r d i n gt ot 1 1 ee x t e n d e dp m p e m e s f u r t h 黜o r e 也em e m o dd e s c r i b e st l l ep r o p e r t i e so f p n om o d e lu s i n gt e i i l p o r a ll o 百c f i n a l l y ，也em 咖o dt r a i l l s f h sm ep n oi n t oa 矗n i t es t a t ct r i m s i t i o ns y s t 啪o fs m v p r o g r a mt h m u 曲a na l g o r i t l 蚰p n 0 2 s m vf o rv 喇聊n gw h e t l l c rt h ef i n i t es t a t e 打a n s i d o ns y s t e ms a t i s f i e st l l et 锄p o r a ll o 舀cf o m m l aw h i c hd c l l o t c st h es y s t e m s p r 叩e m e s ，t h u sc l l s u r e st h ec 0 h 弓c n l e s sa tt l l es p e c i f i c a t i o nl e v e l u s i n gt h ep r o p o s e dm d h o d ，t h i sp 印e rv 舐f i c s 也ec o n s i s t e n c yb e t w e e n 也et r a i n 0 p e r a d o np e 雠n e tw i mo b j e c t s ( t o p n o ) a l l di t sp r o p e n i e s n e 锄p m c a l r e s u l t s o nt l ec a s eo far a i l w a yn e t w o r ka 1 1 dat r a i no p e r a t i o nc h a r ts h o wt 1 1 a tt h ep r o p o s e d m e m o di sc 印a b l eo fr e v e a l i 芏1 9p o t e n t i a lp r o b l c m sa tar n u c he a r l i c rs t a g ei nt h e s y s t e md e v d o p m e n tp r o c e s sa 1 1 de n s u r i n gm ec o i t e c t n e s sa tm es p e c m c a t i o n1 e v d n u sah i 曲d e 留r e eo f 础e 鲥t yi nd e s i 朗a n dv e r i f i c a t i o ni sa c h j e v e d k e y w o r d s ：p e mn e t s 谢t h0 b j e c t s ，t r a i no p e r a t i 彻p e 砸n e t 丽t l lo b j c c t s ，s m v m o d e l i n g ，v 耐f y 郑重声明 奉学位论文是在导师指导下独立撰写并完成的。除文中 已经注明引用的内容外，本论文不含任何其他个人或集体已 经发表或撰写过的作品或成果。学位论文没有剽窃、抄袭等 违反学术道德、学术规范的侵权行为，否则，本人愿意承担 由此产生的一切责任和法律后果。特此郑重声明。 第一章绪论一类对象p e 岍网建模与验证方法研究 第一章绪论 软件的建模与验证是近几年软件工程领域最活跃的研究课题之一。本文将时 态逻辑引入p n o 模型，提出了相应的建模及验证方法。其中，建模方法使用精 确标识p n o 描述系统体系结构模型，并通过时态逻辑定义模型上的需求和限制。 验证方法利用符号验证工具检查p n o 模型和时态逻辑之间的一致性，以确保系 统设计的正确性。 1 1 形式化建模及验证方法的研究现状 目前软件系统建模大都采用图形化语言从宏观上刻画系统的模型结构，而在 某些局部使用自然语言或半形式化语言。这种建模方法比较宜观、易于理解、便 于表达和使用。但是，采用图形化语言构筑的模型往往存在难以发现的模糊性或 歧义性等问题，而这些问题将直接影响系统的安全性与可靠性。形式化方法能在 早期发现系统描述中不一致、不明确或不完整之处，有助于增加软件开发人员对 系统的理解，己被证明是一种行之有效的减少设计错误、提高软件系统可靠性的 重要途径。 所谓形式化方法，是指建立在逻辑、代数、自动机、图论等数学基础上的软 件开发方法，它通过揭示系统的不一致性、二义性及不完全性，使软件系统具有 较高的可信度和正确性，并能使系统具有良好的结构，能较好地满足用户要求 【lj ”。形式化方法的重要研究内容是形式规约和形式验证。形式规约是对程序“做 什么”的数学描述，它通过具有精确语义的形式语言描述程序的功能，是设计和 编写程序的出发点，也是验证程序正确与否的依据。形式验证用来分析己有系统 是否满足形式规约的要求，是形式化方法所要解决的核心问题。基于逻辑和基于 图论的方法是当前常用的两类形式化方法。 基于逻辑的形式化方法使用逻辑描述程序行为的低级规范、使用与时间相关 的行为规范描述系统特性。常用的逻辑方法有基于线性时态逻辑( l i 媳a r1 1 e m p o r a l l o g i c ) 的方法 3 _ 5 1 和基于分支时态逻辑( b m i l c h i n gt e m p o m ll o 百c ) 的方法m 1 两类。 基于逻辑的分析方法能够模拟系统的动念现象，应用公理的形式明确表达系统的 行为性质。但是，基于逻辑的形式化方法主要针对系统运行机制，不能很好地体 第一章绪论一类对象p e 岍网建模与验证方法研究 现系统的物理结构；并且基于逻辑的形式化方法的描述与验证过程过于抽象，既 不便于系统结构的设计和调整，也不易被系统的开发和应用者掌握。 基于网络的形式化方法根据网络中的数据流给出系统模型及网络各结点间 的转换条件，包括谓词变换网、p e 缸网等。目前，使用广泛的网络形式化方法 是p e 踊网睁“】。p e 缸网具有图形的表示方式，能直观地描绘系统的结构特性， 比较容易学习和理解。p e 缸网还有一套成熟的数学理论工具，建立了许多分析 技术，包括可达性分析、不变量分析、保持特性的变换f 包括化简) 、构造理论、 形式语言理论、同步距离及网的分勰和等价。可以借助p e 缸网的描述形式表示 和分析系统的动态行为性质：借助p e t r i 网的代数分析技术刻画系统的结构，建 立状态可达的线性系统关系；借助p c 仃j 网的图分析技术展现系统的运行机制、 分析系统的动态行为；借助p e m 网的归纳分析技术缩小系统的可达状态空间、 降低系统分析的复杂度。随着p e 缸网技术的发展和完善，涌现出了多种扩展的 p e 缸网形式，如着色刚、时间p e 砸网f 1 3 l 、对象网1 1 4 l 【1 5 】、随机p e 仃i 网等， 使得p e m 网的模拟能力和分析能力不断增强。 基于逻辑的形式化方法可以验证系统的属性，但需要对系统进行高级抽象， 不便于系统结构的设计和调整，应用范围受到一定的限制。p c t r i 网方法既具有 严格的数学定义又具有可视的图形描述，但不能很好地表达系统属性。为了充分 利用这两种形式化方法的优点，同时避免其不足，在文献 1 7 】中，用时序p e 雠 网描述和分析并发系统的时序性质，并将时序逻辑引入p e 啊网，增加了p e t 订网 的推理能力，使得p e 晡网能够表达和验证系统的时序需求。在文献【1 8 【1 9 1 【2 0 1 中提出的软件体系结构s a m 使用时问p e 砸网或谓词变迁网来描述软件体系结 构，使用时态逻辑来描述系统属性，通过检查两者的一致性确保软件的正确性。 在文献 2 l 】中讨论了将时间p e 缸网转换成时间自动机( t i m c da u t o m a t a ) 的方法，从 而可以利用针对t a 的验证技术验证时间p e m 网。 本文提出的软件建模和验证方法采用对象p c t i i 网描述系统体系结构模型， 使用时态逻辑定义模型的需求和限制，并通过符号模型验证工具验证对象p e t r i 网和时态逻辑之间的一致性。体系结构规定了系统的实现模式，系统需求和限制 说明了系统的正确性标准，因此检查两者的一致性能确保系统设计的正确性，并 能在系统开发过程的更早阶段揭示潜在的错误，从而实现系统设计和分析验证之 间的高度完整性。 第一章绪论一类对象p c 一网建模与验证方法研究 1 2 研究背景及意义 铁路运输作为一种重要的运输方式，在我国国民经济中发挥着重要的作用。 铁路系统的行车指挥人员设计列车的运营方案、编制运行计划图并检验其合理 性。运营方案和运行计划图是否满足各类安全限制和约束条件，能否在列车偏离 运行图时及时有效地调整，这些都需要计算机仿真技术给出答案【2 2 】。铁路智能运 输系统( r i t s ) 已成为当今世界上铁路交通运输发展的前沿，它是通过高效利用与 铁路运输相关的各类资源，以较低的成本达到保障安全、提高运输效率、改善经 营管理和提高服务质量目的的新一代铁路运输系统【2 3 】【2 4 】。 在对铁路智能运输系统进行研究的过程中，应用计算机建模仿真技术构建相 应的系统仿真实验平台，不仅能节省大量人力、物力资源，保证铁路运营实旌的 安全性，也能为行车组织、运营调整提供科学的决策支持：另一方面，面向实际 应用问题的列车群运行仿真系统为智能混杂系统建模和分析理论的研究提供了 有效的实验平台。在铁路运输领域，国外于7 0 年代就开始在和运营相关的科研 工作中采用计算机仿真技术，最初的研究内容主要集中在闭塞区段内列车运行和 调整情况的分析、线路通过能力的评估、通过能力瓶颈区段的识别、交会或越行 时列车优先级的确定、投资分析等方面。 在我国铁路科研领域，计算机系统建模仿真正逐渐得到重视，越来越多的科 研人员和工程设计人员开始认识到在科研工作中采用这种现代化技术手段的重 要性。我国铁路的列车种类繁多、线路形式多样，且高、低速列车混跑运行。因 此，建立不以任何具体路网为背景，具有良好普适性，可以用于我国任一铁路区 段及有轨交通仿真评估的列车运行仿真系统是非常必要的。已经设计并实施的基 于对象p e 晡网、对象p e t d 子网和基于a g e n t 的g n e t 模型、基于模糊时间p e m 网等一系列列车群行为建模和仿真系统的研究【2 5 - 2 9 1 ，为铁路智能运输系统中相关 问题的可靠性分析、资源的可利用性分析、系统运营能力分析和响应时问性能分 析奠定了良好的基础。其中基于a g 翎t 的g - n e t 模型、基于模糊时间p e 砸网的 列车群行为模型已经有了推理和验证算法，能够对列车运行过程的时间不确定性 问题进行定量分析，验证列车运行调整方案的可行性【3 0 l 。但带有对象p e 缸网的 列车运行模型t o p n o 还没有有效的模型验证方法。本文将上述建模与验证方法 应用在1 1 0 p n o 上，有效地实现了对t o p n o 模型中列车运行的可达性、列车到 第一章绪论 一类对象p e 晡网建模与验证方法研究 站时闻、列车在站时间、列车交会等属性的检测验证，并可以根据需要方便地调 整列车运行计划并再次进行验证，直至满足所要求的系统属性。通过在某一列车 运行区域和运行计划上的应用，该算法表现出分析比较全面、转换简便的特点。 1 3 本文的内容与结构 带有对象的p e 砸网( p n o ) 将构成p n 0 的最基本元素和系统的现实元素分离， 系统的对象实例仅作为网的托肯元素，在初始化和验证具体系统时才构建模型中 库所的标识关系，变迁的使能条件和实施过程也较为复杂，到目前还没有很好的 分析方法。为了解决p n o 模型特殊的属性验证问题，本文基于时态逻辑验证扩 展了p n o 模型中对象的属性，细化了p n o 模型中与变迁实施相关的函数，进而 提出了将p n o 模型转换成对应的s m v ( 符号模型验证工具) 程序从而对p n o 模型 进行验证的算法p n 0 2 s m v 。通过在列车运行p n o ( t o p n o ) 模型上的试验表明 该方法是有效的。 本文按照如下结构组织。 第一章：绪沦。 第二章：相关知识。这一章主要介绍本文涉及到的相关理论。包括p e m 网 基本理论、常用p e 砸网分析验证工具、时态逻辑与符号模型验证工具s m v 等。 其中2 1 节介绍了基本p e 埘网理论，可达树和矩阵方程分析方法的功能和限制； 2 2 节介绍了时态逻辑的概念及时态操作符；2 3 节介绍了常见的p e t r i 网专用分 析验证工具及模型验证工具s m v 的功能特点及其工作原理。 第三章：精确标识p n o 的建模及验证方法。本章首先给出了精确标识p n o 的定义；然后提出了基于验证扩展p n o 模型属性、细化附加条件函数c o n j 和 处理函数爿c f f d 的方法：在此基础上提出将精确标识p n o 转换成对应s m v 程 序以进行分析验证扩展精确标识p n o 模型的算法p n 0 2 s m v ；最后是算法 p n 0 2 s m v 的说明。 第四章：将第三章提出的建模及验证方法应用在列车运行p n o ( t o p n o 、模 型上。首先基于验证扩展了t o p n o 模型中对象的属性，细化了t o p n o 模型中 与变迁实施相关的函数，并定义了控制模型中对象实例之间隶属和约束关系的列 车运行图，进而通过算法p n 0 2 s m v 将扩展的t o p n o 模型转换成对应的 s m v ( 符号模型验证工具) 程序从而对t o p n o 模型进行验证。使用该方法能验证 4 第一章绪论 一类对象p e 矾网建模与验证方法研究 t o p n 0 模型的以下属性：列车运行的可达性、安全性、列车到达时间、列车群 运行过程中的列车交会。通过在某一列车运行区域和运行计划上的应用，该方法 表现出分析比较全面、转换简便的特点。 最后是总结与未来的工作。 第= 章相关知识一类对象p t i 网建模与验证方法研究 第二章相关知识 p e 扛i 网既有直观的图形表示方式，又有成熟的数学理论工具和多种分析技 术。时态逻辑将时间因素引入普通逻辑，从而能处理含有时间信息的命题和谓词。 在模型验证方法中，系统规范被描述成命题时态逻辑公式，系统被模型化为状态 转换系统，通过使用高效的搜索算法来判定规范是否在系统中成立。s m v 是一 个功能强大的符号模型验证工具，最初主要应用于通讯协议和硬件系统的验证， 目前在p e m 网验证方面已展现出强大生命力。 2 1p e t r i 网理论 p e 缸网是一种以图形形式研究系统组织结构和动态特性的理论”，出 c a p e 蛹先生于1 9 6 2 年在他的博士论文中提出。p e m 网理论既有直观的图形表 示方式又有严格的数学理论基础和分析方法，支持系统模型各种性质的分析和性 能的评价，能够对具有并行( p a r a l l d i s m ) 、并发( c o n c u r r 锄c y ) 、同步 ( s ”d 啪i l i z a t i o n ) 、资源共享( r e s o u r c cs h 耐n g ) 等特性的系统建立模型。p e t r i 网广 泛应用于软件体系结构、软件工程、知识表达与推理、并行计算、网络通信协议、 柔性制造系统的建模、分析、控制领域。 2 1 1 p e t r i 网的定义 下面给出p e t r i 网及相关定义【9 _ l “。 定义2 1p e 缸网 p e t r i 网是一个三元组，尸 ( p ，乃一，相应符号的含义如下： ( 1 ) 仁扣l 拙，拂) 为有限的库所集： ( 2 ) 仁 f l ，龟，矗) 为有限的变迁集： ( 3 ) p n 严( 集合p 和集合丁不相交) ，p u 降( 集合p 和集合r 不同时为 空) ； ( 4 ) 埏( a 乃u ( a p ) ( 流关系仅存在元素p 和r 之间，f 中的元素称为弧) ； ( 5 ) d o m ( d uc o d ( 叼叩u 玎不存在孤立元素，d o m ( d = 扛i 砂：0 ) 毋；c o d ( 叼= 洲砂：o ，功毋；搀 p ur 是网元素的集合) 6 第二章相关知识一类对象p e 耐网建模与验证方法研究 定义2 2 前置集和后置集 令p h 尸耳一是一个网，且z z 那么，工的前置集心和后置集d 分别 = 秒f d 力f ) ； 0 0 ) = 9 f 0 毋。 定义2 3p e 血网系统( 西 六元组乏( p ，强巩誓) 是一个p e 砸网系统i 越当且仅当) ： ( 1 ) ( p ，z 抑是一个网； ( 2 ) 量：p 一 1 ，2 ，3 ，) 是库所容量函数； ( 3 ) 肌f 一( 1 ，2 ，3 ，) 是弧权函数； ( 4 ) ：p 一 o ，1 ，2 ，3 ，) 是初始标识，满足：v p ：( 力型【) 。 ( 5 ) 函数肘：p 一 0 ，1 ，2 ，3 ，) 是毋拘标识i m 坳p ：肘c 力型r p ) 。 在p e 硒网的图形表示中，对于弧，f p 1 时，将 坳标注在弧上。根 据足函数的取值可将p e t r i 网分为无界网和有界网，如果置可取m ，则p e 廿i 网是 定义2 4 变迁的使能和触发( e n a b l i n ga n df 讯n 曲 乎c p ，正f ，彬墨) 是一个p e t r i 网系统。 ( 1 ) 一个变迁拒r 在标识m 下是使能的， i 仃 v 口p ： ( 2 ) 变迁f 丁在标识m 下是使能的，在f 触发后产生一个新的后继标识埘， 凹可由下列方程给出：b p ：协) = 肘p ) 一阡协，0 + 职f ) ；实际上f 的触 发仅对其前置集和后置集以0 、0 ( 0 中的“托肯”数量有影响。也可用下 i 坳) - 阡p ，o ，p 厦f ) 炉萑o ( f ) i j 坳) + 坝印) ， p o ( 力，p 芒“力 【 脚卜1 川卅职慨 p 喇n d ( f ) 广 m ，其它l ( 3 ) 系统标识m 经过f 的触发得到新的标识m ，可以表示成 研f m 。 第二章相关知识一类对象p e 啊网建模与验证方法研究 2 1 2p e t r i 网基本性质及分析方法 p e 晡网有一套成熟的数学理论工具，支持系统模型各种性质的分析和性能 的评价。使用这些分析方法可以刻画系统的结构，展现系统的运行机制，表示和 分析系统的动态行为，降低系统分析的复杂度。 1 p e t r i 网的基本性质 p e 晡网的基本性质主要体现在可达性、有界性、安全性和活性等方面，这 些性质充分体现了系统性能、结构和行为之间的对应关系【9 】 1 0 1 。 定义2 5 可达性 对一个给定初始标识即初始托肯( t o k e l l ) 标识硒的p e 砸网( v 舶) ，可达集 r ( m ) 表示该p e 喇网在初始状态标识下，触发所有变迁可到达的状态标识 集合。r ( 删i ) 既取决于网的结构，也取决于网的初始状态标识。直观上看，一 个状态标识即托肯分布 矗为可达意味着，在给定的初始标识下经过有限次 变迁触发到达托肯分布j 】l 矗。 定义2 6 有界性 p c 仃j 网( a 动是尽有界的，i 行v m r u v 舶) ，b p ：朋p ) 兰彤，其中 厅 1 ，2 ，3 ，) 。有界性意味着在所有可能的状态标识下，p e 晡网中库所节点的托 肯数必为有界。 定义2 7 安全性 1 有界p e 砸网是安全的，它是一种晟为苛刻的有界性。如果在初始标识的 任何可达集里，一个库所的托肯数都不超过1 ，则称该库所都是安全的。如果一 个p e 砸网的每一个库所都是安全的，则称该p “网是安全的。 定义2 8 活性 如果从经若干次变迁触发到达的任一标识尬，网中存在触发序列使所有 变迁都能触发，那么称该p e 砸网( _ 嬲) 是活性的( 或者说，肘j 对来说是个活 性的标识) 。 2 p e t r i 网的常用分析方法 p e m 网有一套成熟的数学理论工具，建立了许多分析技术，包括可达性分 析、不变量分析、保持特性的变换( 包括化简) 、构造理论、形式语言理论、同步 距离及网的分解和等价。使用这些分析方法可以刻画系统的结构，展现系统的运 第二章相关知识一类对象p e 砸网建模与验证方法研究 行机制，表示和分析系统的动态行为，降低系统分析的复杂度。 ( 1 ) 可达树技术 从一个给定p e t i i 网的初始状态j l 而出发，触发使能变迁能得到多个新标识， 从这些新标识出发再次触发使能变迁能得到更多的标识。如此类推，可以得到由 p e 缸网可达标识组成的可达树。可达树的节点代表从初始标识出发得到的所有 标识，弧线代表触发的变迁。 当p e 缸网无界时，不可能得到p e 缸网的所有可达标识。为了用有限的形式 表达有无限个状态的系统的运行情况，需要引入一个表示无界量的符号缈。具 有这样的性质：对于所有n ，n = 打m e c 0 n d ：s f t r n e x t j e c t t o na n dt r n e x t j e c t i o n p l n n t i m e = n m e n 故8 ) ：乃c “ 万。加如押d 0 缸砌以) a n dn 以甜u 砌以= ( 3 ) 变迁处理函数彳c 打伽的细化 根据增加的对象属性细化模型中变迁附加条件函数c b ”d ，如下所示： a c t i o n o ：t r c t r r e n t j 删。萨s 铷碡n 删帆h t j e c t i o 咖a n dt r s 搬r l j i m e = f 加8a 1 1 d 研f m 加= 什a i l d & 加加= 西。 a c l i o n t ：t r 叫r r e n u 埘蛀。舻妒a n d 西c t l r r e m j e c t i o 萨s e 觚dn s t 倪r f j i m e = 盯聊8a n d 打谊f m = 西a n d & f ，口加= z 卜。 第四章t o p n 0 的建横与验证 一类对象p e 啊网建模与验证方法研究 一谢细) ：孤c 柳钥。胁砌萨锄d 弘删 铆坐伽矿a n d 鼹抛栩= 一a 1 1 d 弘s 肋胁w 萨功钾口a 2 列车运行图 t o p n o 模型将构成p n o 的最基本元素和路网元素分离；构成路网的对象实 例由一系列醐t 。n 、胁加、c 豳n 等对象实例构成；各实例之问存在一定的约 束关系。为了表示这些实例之间的隶属和约束关系，本文定义了称为列车运行图 的矩阵。 定义4 2 列车运行图 列车运行图是表示列车、站台、区域对象实例之间关系的矩阵。设t o p n o 模型中共有台列车、m 个站台、s 个运行区域，列车运行图是一个+ 的矩阵，如下所示： 尸1 1 p 2 1 风1 p 1 2 p 2 i p n 2 毖繁：般：糍1 p 2 p 2 m 1p 2 胛p 2 - m + s 岛 p n mp n m 十、p n 埘+ 2 p m m + sj 列车运行图的每一行对应一台列车的运行计划，每一列对应一个站台或区域 桷蘸请谜。p 产岱e q h e n c e ，t 融r r “口l n m e j ，p l n n 翼掣豇m e j s s t j 妞t i o t 、，为 列车在站台或区域的点计划。其中： & 叮“酬c g 为该点在列车运行中的次序，用自然数表示。列车从& g “口n c 8 为1 的车站或区域出发，依次通过口“g n 饱为2 、3 的车站或区域直到 终点； 对站台计划而言，尸肠n 彳州阳，刀m e 为列车的计划到站时间；对区域计 划而言，砌n 彳r 一似，肋船为列车的计划发车时间。因为时间的不确定 性，用时间区间( 如【1 ，2 】) 表示p f d n f v n l 硒竹8 ； p 肠n j 啦l 砌卯为列车的计划停留时间( 对车站而言) 或计划运行时间( 对 区域而言) ，用自然数表示。 腰三f 口踟w 为列车在该点的作业类型，o 表示非终点，1 表示终点。 算法4 1 计算列车的下一停靠站台，对每一列车执行以下运算：如果列车的 c “，m ” 妣i 砌h 属性为空( 列车不在某一站台停靠) 或当前时刻小于列车的发车时 间与列车计划运行时间之和( 列车还没有运行到车站) ，则置列车的下一停靠站台 ，i 舞戮孵一筵i 蓊嚣嚣意瀚& 。 ，。1。l 第四章t o p n 0 的建模与验证 一类对象p c 岍网建模与验证方法研究 为空( s t e p1 3 ) ；否则根据列车运行计划确定列车的下一车站：如果当前时刻大于 列车在该车站的砌n4 州f 矗m p 值( 已到计划到站时间) 且站台的f r a 抽属性为 空( 站台上没有停放列车) ，则置列车的下一停靠站台为该站台( s t e p1 4 1 - s t 印 1 4 ，2 、。 算法4 1 ：计算列车的下一停靠站台 输入：列车对象实例集合m 跏、站台对象实例集合鼬口砌一、列车运行图 p l 口n 输出：列车对象实例集合m 胁 s t 印1 ) 对砌胁的每一列车对象丹，执行步骤1 1 一1 4 s t e p1 1 ) l n 在j 弹的行标 s t 印1 2 ) ，一乃c “，陀n f - 8 c 如n 在j 打的列标 s t 印1 3 ) 如果( n c “w n t 缸砌n ! = 庐或f 砌f ；p k 月 订 同p 肠叫州，哪l 刀m 0 ，则 脚h “t m n o n + s t ； s t e p2 ) 返回( z h 妇) 算法4 2 计算列车的下一运行区域，其运算步骤为：如果列车的 洲e n t 缸f f d n 属性非空( 列车在某站台停靠) 且列车在该站台的趣邪o 舭m 值 为1 ( 当前站台是终点站) ，则下一运行区域为痧，代表到达终点( s f 印1 3 ) ；否则， 如果列车的“n fs m 如n 属性非空( 列车在某站台停靠) 且当前时刻还没到列车 的到站时间与列车计划停靠时间之和( 还没到发车时间) ，则列车的下一运行区域 置为一1 ( s t 印1 4 ) ；否则，根据列车计划确定列车的下一运行区域：如果当前时刻 大于列车在该区域的肋h j 州m l z 砌e 值( 已到计划到沾时间) ，将列车下一运行 区域设置为该区域( s t 印1 5 1 一s t 印1 5 2 ) 。 算法4 2 ：计算列车的下一运行区域 输入：列车对象实例集合丁h 跏、区域对象实例集合鼬c 砌雎、列车运行图 第四章t 。p n o 的建模与验证 类对象p 谢i 网建模与验证方法研究 p l n n 输出：列车对象实例集合打衲l s t c p1 ) 对打砌l 的每一列车对象打，执行步骤1 1 - 1 4 s t e p1 1 ) f 一乃在p 缸雄的行标 s 卸1 2 ) - ，一乃c 删t 缸f 泐l 在胁一的列标 s t 印1 3 ) 如果( n c “r 陀h t 招勘n ! = 妒且j 一【f d 1 西一l 蚍如，z = 1 ) t r n e x j e c t i o n 一咖 s t 印1 4 ) 如果( 行删r m h t 凹踟n ! = 且 f 折l p = 行j 胁蔬晰p + j 肼【f 】们p ? 口以j 哑五m 0 乃n 哦，p 咖n 一- 1 s t 印1 5 ) 否则，对& 蹦鲫的每一站台对象& ，执行步骤1 5 1 1 5 - 2 s t c p1 5 1 ) 七一& 在川鲫的列标 s t e p1 5 2 ) 如果( p f 口一嘲嘲j 叼 锄c 萨胁斗【f 阴3 叼”柳c 时1 且 砌l 驴= p 肠栉 司嗣讹叫删m l 砌”力 砰h “i e c 如，i 一& ； s t 印2 ) 返回( 砌抽) 3 扩展t o p n o 模型的属性 在对t o p n o 模型进行验证时，需要验证与列车对象相关的属性，如列车的 可达性、列车到站时间、列车在站时间等属性。就列车运行而言，只有在所有列 车都能到达终点的情况下对系统属性的验证刁+ 有意义。本文定义了如下t o p n o 模型的属性： 定义4 3 列车的弱可达性 指存在一个列车运行序列，使得列车对象办能到达终点。可用如下时态逻 辑公式表示： 了o ( 挣s 啦p ( p 0 ) 定义4 4 列车的强可达性 指对于任何列车运行序列，列车对象都能到达终点。可用如下时态逻辑表示： v o ( 丹s 雌烈m ) 定义4 5 列车到站时间 指在所有列车都能到达终点的前提下，列车在某一时刻到达车站。例如列车 第删章t d p n o 的建模与验证 一类对象p e 晡网建模与验证方法研究 打到达站的时间是l 那么对于任何列车运行顺序，所有列车必定能到达终 点站( 强可达) ，这一属性可用如下时态逻辑表示： ( 韵( 丹硎脚n o 细加以 弘s 缸疋砌f d ) ( v 口( ( 乃删脚以。胁砌2 弘砌r o 拥f 力寸v o ( 对所有办d ( 7 h 加) ，有乃j 卿( | p 功) ) ) 同样，如果开到达站的时间是l 那么存在一个列车运行顺序，使得所 有列车能到达终点站( 弱可达) ，这一属性可用如下时态逻辑表示： ( j o ( n c 聊硎t m 如h 乃础z r o 咖f 即) ( v o ( ( n c “，地n t 胁“d 开 丹础i t 砌4 f 乃斗j o ( 对所有n d ( m 加) ，有纷s 唧( p 们) ) ) 定义4 6 列车在站时间 指在所有列车都能到达终点的前提下，列车在某一时刻停靠在车站。例如列 车丹在n 亚之间的任一时刻停靠在站，那么存在一个列车运行顺序，使得 所有列车能到达终点站，这一系统属性可用如下时态逻辑表示： 对于所有的t 【n ，死 ( j o ( 时钟= r 丹翻删刀。加f f d 胛跚) ( v o ( ( 时钟= r 乃c “胱以。埘砌竹e 踟寸j o ( 对所有抒d ( m f n ) ，有乃j 卿( p f 一) ) ) 定义4 7 列车交会 指两列或多列列车同时停靠在某一车站。例如验证列车丹1 和打2 能否在车 站& 交会，可用如下逻辑公式表示： j ot n l 甜r r e m j t a n o n s t t ，2 c h r r e n t j t n n o n s 如 定义4 8 列车运行的安全性 列车运行的安全性指列车运行过程中要保证任何两列列车不能同时在同一 站台停靠或同时在同一区域中运行。可用如下逻辑公式表示任何两列列车不能同 时在同一站台停靠： 对于所有的n 1 d ( m 加) ，z 挖d ( m m ) ，乃1 z 挖，有 v 口_ 1 ( 护1 c “，阳n t 胁加以= 眈c z 胛伽t 胁咖玎 护1 c “，r 阴f 埘矗d n 彩； 可用如下逻辑公式表示任何两列列车不能同时在同一站台停靠： 对于所有的n 1 d ( z 妇f ) ，m d ( m 加) ，乃1 z 挖，有 d q n c u r r e n t j e c t i o h = t r 2 c h r r e m j e c t i o n 亡r 1 c t t r r e n t j e c t t o n 钠| 第四章m p n o 的建模与验证 一类对象p e 岍网建模与验证方法研究 4 2 2t o p n o 到s m v 程序的转换说明 t o p n o 作为精确标识p n o 的一个特例，可根据算法3 1 从t o p n 0 模型的 定义出发得到相应的s m v 程序。下面重点说明程序中时间的表示及处理，对象 实例d 、库所p 、变迁a 变量矿在s m v 中的表示方法，以及变迁o l 、f 2 、如的 实施过程。 1 转换程序的时间表示及处理 铁路智能运输系统中构成系统主体的列车群并发性的表述、面向不同分析问 题的系统混合属性的处理、影响列车群运行的各种不确定性因素的处理均涉及到 对时间参数的分析，因此在模型验证时要能表示并处理与时间有关的属性。由于 存在影响列车运行的多种不确定因素，列车并不能完全按运行图确定的时问运 行，因此如何有效表示时间就成为验证的关键问题，也是难点问题。为此，在验 证程序中定义了一个时钟变量，并采用时闻区间来控制列车运行。在模拟模型的 状态变迁过程中，如果在某一时刻存在多个使能变迁，则随机触发一个使能变迁； 如果不存在使能变迁，则在下一状态将时钟变量的值增加l 。 2 t o p n 0 的对象实例o 、库所p 、变迁扎变量y 在转换程序中的表示 根据算法3 1 的s t 印1 1 s t e p1 4 ，需要分别在s m v 程序中定义与t o p n o 模型中类m m 、s 缸f f o 玑觑砌”对应的结构体铆旭一z 勉加、0 p g j 钯肋n ， 卯口，跆甜d n 及对应的对象实例数组跏匕了h 跏、s m 匕跏砌n 、跏匕& 砸肼；定 义与库所p ，凇、m 、a p 、r ，、n f 对应的一维布尔数组肋i v 砌s 、5 锄vn 口、 s 锄v 胁、跏va r 、m v 脚。并根据对象的初始值和初始状念下库所的托肯值 设置上述数组的初始值。 此外，还要在s m v 程序中定义与模型变量办、& 、对应的变量5 如v 打、 s 锄y j 趴胁- 野，这些变量的取值范围分别在0 到i d ( 加抽) l 、o 到i d 0 口c 打m ) l 、o 到1 d ( s 加幻n ) 窿间。 3 转换程序中状态变迁的实旅 在t o p n o 中，变迁的实旌将实例化该变迁的前相关函数和后相关函数；设 置变迁的前置库所和后置库所下一状态的值；执行变迁的4 甜o n 函数，并修改所 涉及对象的属性。下面说明t o p n 0 中列车进站、出站和到达终点的处理。 ( 1 1 列车进站处理 第四章t o p n o 的建模与验证一类对象p e 砸网建模与验证方法研究 列车迸站对应变迁f 1 ，根据t o p