一种基于有限精度时间自动机的模型检测工具  

Model-checking Tool Based on Finite Precision Timed Automata (FPTA)

作　　者：徐雨波[1] 晏荣杰[1] 

机构地区：[1]中国科学院软件研究所计算机科学国家重点实验室

出　　处：《计算机应用研究》2006年第5期121-125,共5页Application Research of Computers

基　　金：国家自然科学基金资助项目(60273025);国家"973"计划资助项目(2002CB312200)

摘　　要：基于有限精度时间自动机模型,实现了一种新的数据结构———SDS,用SDS符号化表示状态空间的实时系统模型检测工具,并进行了初步的实验分析,取得了良好的效果。Based on the theory of Finite Precision Timed Automata （FPTA）, this article implements a kind of data structure, named series of delay sequence （SDS） , to describe the state space symbolically. Then implement a model-checking tool for real-time systems based on the data structure of SDS. From primary experiment results, it can be concluded that the performance of the tool is good in most cases.

关 键 词：模型检测工具 实时系统 数据结构 有限精度 时间自动机 

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]