基于UPPAAL的复杂定时数据建模-论文.pdf

《基于UPPAAL的复杂定时数据建模-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、第25卷第4期中原工学院学报V01．25NO．42014年8月JOURNALOFZHONGYUANUNIVERSITYOFTECHNOLOGYAug．，2014文章编号：1671—6906(2014)04—0028～05基于UPPAAL的复杂定时数据建模李真，王从银，庄雷(1．郑州大学信息X-程学院，郑州450001；2．吉首大学数学与计算机科学学院，湖南吉首416000)摘要：针对路由协议中复杂定时数据建模的难题，提出一种基于离散和抽象的建模方法。该建模方法中，各条复杂定时数据的生存时间被离散化为时间分

2、片，并用时间分片数量表示对应数据的生存时间。采用轮询策略周期性地检查数据的生存时间并更新数据。以路由协议中的链路保持特性为例，在建模过程中运用所提出的方法，对路由协议的链路保持功能和链路断开的敏感性进行验证。结果表明，这种建模方法可应用于复杂定时数据的建模。关键词：时间自动机；UPPAAL；建模；时间分片中图分类号：TP301文献标志码：ADOI：10．3969／j．issn．1671—6906．2014．04．007模型检测技术是一种形式化验证技术，不同的建模方法具有不同的特点。进程代数方法在验证协议的

3、1相关知识交互行为方面具有优势，但不利于对协议的时问行为进行验证。基于时间自动机的建模方法是对协议的时时间自动机是自动机的扩展，在传统自动机的迁间行为进行建模的主流方法，UPPAAL是其代表性建移系统中加入了延时迁移功能，用于描述时间的流模工具，是高效的实时系统验证工具。其典型的应用逝l_4]。UPPAAL工具进一步增强了时间自动机的功例子有TDMA协议的启动机制验证_1]、Bang&能，在建模时加入变量和类似于C语言语法的自定义Olufsen公司的音视频系统故障]、变速箱的自动验函数，以便更容易地描述待

4、验证系统[5]。很多带有数证Ⅲ等。组变量的模型都采用专门的自动机来管理数据结构，用UPPAAL对带有一定生存时间的多个同类数使得模型能以简单的方式管理复杂的数据[6]。虽然加据进行描述时，现有的建模方法并不能很好地应用。入了变量并且支持数组和结构体类型，但UPPAAL一般地，UPPAAL表示有一定生存时间的一条数据或工具提供的变量管理机制并不支持定时数据。而对于其行为时，采用时间自动机在模型内部直接描述的方网络协议来说，时效性是必须考虑的问题，因此本文提法，以便将数据的行为完全内嵌到系统模型中。其优出了一

5、种为多条数据时效性建模的方法。势是简单和高效，但对于具有不同生存时间的多条数时间自动机的定义(定义1)：一个时间自动机是据进行建模时，这种方法却不再适用。这一方面在于一个五元组<，S，S。，C，E>，其中是有限的字母此方法须为每条数据提供若干控制位置，会显著增大表，S是状态的一个有限集，S。S是开始状态的集模型规模；另一方面因为此方法的灵活性差，不能适应合，C是时钟的有限集合，ES×S××2×(C)是数据的随机存储和处理，使整个系统的可扩展性变差。迁移的集合。边表示输入字符是a时，在路由

6、协议的特殊情况下，甚至难以用现有方法进行从状态s到状态s的迁移。建模。本文的关键在于提出一种基于时间分片的解决UPPAAL中扩展了时间自动机的表达能力，其定方法。义(定义2)如下：UPPAAL中的时间自动机是一个七收稿日期：2014—04—30基金项目：河南省科技攻关项目(12210221OO42)作者简介：李真(1987一)，男，河南南阳人，硕士生，主要研究方向为模型检测。第4期李真，等：基于UPPAAL的复杂定时数据建模元组，其中s是有限集合，s。E网络中有若干路由器，上面运

7、行着oLsR路由协s表示初始状态，A是动作的集合，C是时钟的有限集议。每个路由器维护着各自的链路信息、邻居信息、拓合，V是数据变量的集合，：s一(C，)将一个状态扑信息和路由信息等。为简化模型，这里只考虑链路映射为一个不变式(invariant)，Ec_S×(C，)×A×信息。LinkSet是链路信息的集合，路由器通过Link—R(C，)×S是边的集合。Set维护链路信息。每条链路信息就是一个五元组linkTuple：一

8、time，LASYMtime，L2问题描述—————time>。其中：L—local—iface—addr表示路由器的本地接口地址；Lneigh——iface—addr表示与此路由器通信的邻居路2．1定时数据及其应用由器的接口地址；L—SYM—time表示链路状态是双向在OLSR等adhoc路由协议中，路由器要存储关的生存时间；L～ASYM—time表示链路状态是单向的于链路和拓扑的各种信息。这些信息分别以链路集合生存时间；L