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

作     者：钱俊彦 赵岭忠 QIAN Jun-yan;ZHAO Ling-zhong

作者机构：桂林电子工业学院计算机系广西桂林541004 

基　　金：国防"十五"预先研究项目基金资助 

出 版 物：《计算机应用研究》 (Application Research of Computers)

年 卷 期：2005年第22卷第7期

页      码：68-70页

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

主 题 词：模型检验 时间自动机 TCTL 

学科分类：08[工学] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1001-3695.2005.07.024

馆 藏 号：203141741...