| 时间自动机可达性分析算法的改进 |
| |
| 引用本文： | 张松年 庄雷 杜娟. 时间自动机可达性分析算法的改进[J]. 计算机工程与科学, 2007, 29(10): 44-46 |
| |
| 作者姓名： | 张松年 庄雷 杜娟 |
| |
| 作者单位： | 郑州大学信息工程学院,河南,郑州,450001;郑州大学信息工程学院,河南,郑州,450001;郑州大学信息工程学院,河南,郑州,450001 |
| |
| 摘 要： | 模型检测时,实时系统的大多数安全属性和部分活性都可以通过可达性分析算法来验证。本文介绍了时间自动机和可达性分析算法,并对可达性分析算法中的后继算法进行了改进。
|
| 关 键 词： | 时间自动机 可达性分析 后继 |
| 文章编号： | 1007-130X（2007）10-0044-03 |
| 修稿时间： | 2007-03-29 |
Improvement on a Reachability Analysis Algorithm in Timed Automata |
| |
| ZHANG Song-nian,ZHUANG Lei,DU Juan. Improvement on a Reachability Analysis Algorithm in Timed Automata[J]. Computer Engineering & Science, 2007, 29(10): 44-46 |
| |
| Authors: | ZHANG Song-nian ZHUANG Lei DU Juan |
| |
| Affiliation: | School of Computer Engineering and Science, Zhengzhou University, Zhenzhou 450001,China |
| |
| Abstract: | For most safety properties and some liveness properties of real-time systems,model checking can be reduced to reachability analysis.In his paper,we introduce timed automata and the algorithm of reachability analysis,and proposes an improvement algorithm of the basic successor algorithm. |
| |
| Keywords: | timed automata reachability analysis successor |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载免费的PDF全文 |
