基于UPPAAL的复杂定时数据建模  

Modelling Complex Timed Data Based on UPPAAL

作　　者：李真[1] 王从银[1,2] 庄雷[1] 

机构地区：[1]郑州大学信息工程学院,郑州450001 [2]吉首大学数学与计算机科学学院,湖南吉首416000

出　　处：《中原工学院学报》2014年第4期28-32,共5页Journal of Zhongyuan University of Technology

基　　金：河南省科技攻关项目(122102210042)

摘　　要：针对路由协议中复杂定时数据建模的难题,提出一种基于离散和抽象的建模方法。该建模方法中,各条复杂定时数据的生存时间被离散化为时间分片,并用时间分片数量表示对应数据的生存时间。采用轮询策略周期性地检查数据的生存时间并更新数据。以路由协议中的链路保持特性为例,在建模过程中运用所提出的方法,对路由协议的链路保持功能和链路断开的敏感性进行验证。结果表明,这种建模方法可应用于复杂定时数据的建模。A discretization and abstraction based method is proposed to resovle the problem of modeling complex timed data in routing protocols. The lifetime of each timed data is discretized to time slices, and represended by the amount of the corresponding time slices. Then, the polling strategy is applied to check the lifetime of each data and update it periodically. Finally, take the link hold feature as an example, the proposed method is applied in the modeling process. The verification on function of link hold and of breakage detecting show that the proposed modeling method is a feasible method to modeling complex timed data in practice.

关 键 词：时间自动机 UPPAAL 建模 时间分片 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]