| 有限精度时间自动机的可达性检测 |
| |
| 引用本文： | 晏荣杰,李广元,徐雨波,刘春明,唐稚松.有限精度时间自动机的可达性检测[J].软件学报,2006,17(1):1-10. |
| |
| 作者姓名： | 晏荣杰 李广元 徐雨波 刘春明 唐稚松 |
| |
| 作者单位： | 1. 中国科学院,软件研究所,计算机科学重点实验室,北京,100080;中国科学院,研究生院,北京,100049
2. 中国科学院,软件研究所,计算机科学重点实验室,北京,100080 |
| |
| 基金项目： | 中国科学院资助项目;科技部科研项目 |
| |
| 摘 要： | 为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finite precision timed automata,简称FPTA)作为实时系统的形式模型,并提出了一种数据结构SDS(series of delay sequence)符号化表示状态空间中的状态集.FPTA只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,Alur与Dill提出的时间自动机的可达性检测可简化为FPTA的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了SDS的特点及不足.
|
| 关 键 词： | 有限精度时间自动机 符号化方法 模型检测 可达性 |
| 收稿时间： | 2004-04-28 |
| 修稿时间： | 2004-04-282005-07-11 |
Reachability Checking of Finite Precision Timed Automata |
| |
| Yan RJ,Li GY,Xu YB,Liu CM and Tang ZS.Reachability Checking of Finite Precision Timed Automata[J].Journal of Software,2006,17(1):1-10. |
| |
| Authors: | Yan RJ Li GY Xu YB Liu CM and Tang ZS |
| |
| Affiliation: | 1.Laboratory of Computer Science, Institute of Software, The Chinese Academy of Sciences, Beijing 100080, China; 2.Graduate School, The Chinese Academy of Sciences, Beijing 100049, China |
| |
| Abstract: | To relieve the state space explosion problem, and accelerate the speed of model checking, this paper introduces the concept of finite precision timed automata (FPTAs) and proposes a data structure to represent its symbolic states. FPTAs only record the integer values of clock variables together with the order of their most recent resets to reduce the state space. The constraints under which the reachability checking of a timed automaton can be reduced to that of the corresponding FPTA are provided, and then an algorithm for reachability analysis is presented. Finally, the paper presents some preliminary experimental results, and analyzes the advantages and disadvantages of the new data structure. |
| |
| Keywords: | finite precision timed automata symbolic method model checking reachability |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
