| 题名: | 一种基于离散时间自动机的LTL性质检测工具 |
| 其他题名: | a model checking tool based on discrete timed automata
|
| 作者: | 张文亮
; 彭云全
|
| 关键词: | 离散时间自动机
; 非空性检测
; 线性时序逻辑性质
; 时间自动机
; 检测工具
; Timed Automata
; 状态空间爆炸
; 线性时序逻辑
; 利用模型
; 指数增长
; 压缩存储
; 性质验证
; 系统规模
; 时间空间
; 检测效果
; 检测速度
; 检测过程
; 检测方法
; 存储延迟
; 效率
; 算法
; 实验
; 技术
|
| 刊名: | 计算机仿真
|
| 发表日期: | 2008
|
| 期: | 4, 页:80-83 | | 部门归属: | 中国科学院软件研究所计算机科学国家重点实验室,北京,100080;中国科学院研究生院,北京,100049;中国科学院软件研究所计算机科学国家重点实验室,北京,100080;中国科学院研究生院,北京,100049
|
| 摘要: | 模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点.目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的工具还比较少,且效率都较低.介绍了一种基于离散时间自动机的LTL性质检测工具,采用了在状态空间中存储延迟序列(DS)的技术,对状态进行压缩存储,减小了时间空间的消耗,加快了检测速度.实验表明,该工具的检测效果是不错的,要好于同类工具,如DTSpin. |
| 语种: | 中文
|
| 内容类型: | 期刊论文
|
| URI标识: | http://ir.iscas.ac.cn/handle/311060/10401
|
| Appears in Collections: | 计算机科学国家重点实验室 _期刊论文
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| 一种基于离散时间自动机的LTL性质检测工具.pdf（319KB） | -- | -- | 限制开放 | -- | 联系获取全文 |
|
| Recommended Citation: | |
张文亮,彭云全. 一种基于离散时间自动机的LTL性质检测工具[J]. 计算机仿真,2008-01-01(4):80-83.
|
|
|
