实时时序逻辑语言XYZ/RE到时间自动机的映射  

Mapping from Real-time Temporal Logic Language XYZ/RE to Timed Automata

作　　者：刘珊艳[1,2] 戎玫[3] 张广泉[2,4] 

机构地区：[1]荆楚理工学院计算机学院,荆门448000 [2]重庆师范大学数学与计算机科学学院,重庆400047 [3]暨南大学深圳旅游学院,深圳518053 [4]苏州大学计算机科学与技术学院,苏州215006

出　　处：《微计算机应用》2008年第6期69-75,共7页Microcomputer Applications

基　　金：重庆市自然科学基金项目(CSTC;2006BB2259);重庆市教委科学技术研究项目(批准号:040803);江苏省高校自然科学基金(批准号:05KJB520119)

摘　　要：时间自动机是一种重要的实时系统建模工具。本文建立了实时时序逻辑语言XYZ/RE到时间自动机的一种映射机制,将XYZ/RE所描述的系统进程直接转换为时间自动机,这样不但可以准确捕获实时系统功能和控制行为,还可以利用基于时间自动机的验证工具UPPAAL对XYZ/RE描述的系统正确性进行检测。最后本文通过一个实例的描述与检测,验证了映射机制的有效性。Timed Automata is an important tool for modeling real -time systems. This paper presents a mechanism for mapping real - time temporal logic language XYZ/RE to Timed Automata, translating systems＇ process described by XYZ/RE into Time Automata, then which can not only capture real - time systems＇functionalities and control behaviour precisely, but also can use verified tool based on Timed Automata to check accuracy of the systems described by XYZ/RE. At last, the paper verified the validation of the mechanism by describing and checking an example.

关 键 词：XYZ/RE 实时系统 时间自动机 UPPAAL 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构] TP311.5[自动化与计算机技术—计算机科学与技术]