J4 ›› 2007, Vol. 29 ›› Issue (10): 44-46.
• 论文 • 上一篇 下一篇
张松年 庄雷 杜娟
出版日期:
发布日期:
Online:
Published:
摘要：
模型检测时,实时系统的大多数安全属性和部分活性都可以通过可达性分析算法来验证。本文介绍了时间自动机和可达性分析算法,并对可达性分析算法中的后继算法进行了改进。
关键词: 时间自动机 可达性分析 后继
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.
Key words: （timed automata, reachability analysis, successor）
张松年 庄雷 杜娟. 时间自动机可达性分析算法的改进[J]. J4, 2007, 29(10): 44-46.
0 / / 推荐
导出引用管理器 EndNote|Ris|BibTeX
链接本文: http://joces.nudt.edu.cn/CN/
http://joces.nudt.edu.cn/CN/Y2007/V29/I10/44
