###
DOI:
Journal of Software:2009.20(8):2015-2025

ETL的符号化模型检验
刘万伟,王戟,王昭飞
(国防科学技术大学 计算机学院 并行与分布处理国家重点实验室,湖南 长沙 410073)
Symbolic Model Checking of ETL
LIU Wan-Wei,WANG Ji,WANG Zhao-Fei
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 4425   Download 3763
    Revised:August 11, 2008
> 中文摘要: 为使符号化模型检验技术适用于全部ω-正规性质,研究了ETL(extended temporal logic)的符号化模型检验方法.首先,扩展了LTL(linear temporal logic)的Tableau方法,给出了ETL的Tableau构造方法,进而给出了该方法基于BDD(binary decision diagram)的符号化实现.同时,在NuSMV的基础上实现了支持ETL符号化验证的模型检验工具ENuSMV.该工具允许用户自定义时序连接子,从而可以检验全部ω-正规性质.实验结果表明,ETL性质能够被高效地采用符号化技术加以检验.
Abstract:To make symbolic model checking approach applicable to all ω-regular properties, this paper studies symbolic model checking for ETL (extended temporal logic). First, the Tableau approach for LTL (linear temporal logic) is extended to that of ETL, and then the BDD (binary decision diagram)-based encodings of this technique is given. Moreover, the model checking tool ENuSMV is implemented based on NuSMV, which allows users to customize temporal connectives, and hence all ω-regular properties can be verified. Experimental results show that ETL can also be efficiently verified by the symbolic approach.
文章编号:     中图分类号:    文献标志码:
基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60725206, 60621003 (国家自然科学基金); the National High-Tech Research and Development Plan of China under Grant No.2006AA01Z429 (国家高技术研究发展计划(863)) Supported by the National Natural Science Foundation of China under Grant Nos.60725206, 60621003 (国家自然科学基金); the National High-Tech Research and Development Plan of China under Grant No.2006AA01Z429 (国家高技术研究发展计划(863))
Foundation items:
Reference text:

刘万伟,王戟,王昭飞.ETL的符号化模型检验.软件学报,2009,20(8):2015-2025

LIU Wan-Wei,WANG Ji,WANG Zhao-Fei.Symbolic Model Checking of ETL.Journal of Software,2009,20(8):2015-2025