一种基于时间自动机的域构造方法

• 作者: 赵岭忠 钱俊彦
• 来源期刊: 计算机应用研究
• 关键词: 模型检验 时间自动机 TCTL
• 年，卷（期）: 2005,（7）
• 所属期刊栏目: 研究探讨
• 页码范围: 68-70
• 页数: 3页
• 分类号: TP301
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2005.07.024

摘要

模型检验是一种重要的形式化自动验证技术,通过状态空间搜索来保证软硬件设计的正确性.由于TCTL不是针对时间自动机,而是针对有限状态变迁系统的,从而无法使用TCTL直接对时间自动机进行模型检验.给出了一种从时间自动机到有限状态变迁系统的方法,并在不改变时间自动机的语义上,使时间自动机等价后的域状态数尽可能少,在一定程度上有效地解决了状态空间爆炸问题.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	钱俊彦	桂林电子工业学院计算机系	86	238	9.0	10.0
2	赵岭忠	桂林电子工业学院计算机系	64	229	8.0	11.0