| ETL的符号化模型检验 |
| |
| 引用本文： | 刘万伟,王戟,王昭飞.ETL的符号化模型检验[J].软件学报,2009,20(8):2015-2025. |
| |
| 作者姓名： | 刘万伟 王戟 王昭飞 |
| |
| 作者单位： | 国防科学技术大学,计算机学院,并行与分布处理国家重点实验室,湖南,长沙,410073 |
| |
| 基金项目： | 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)) |
| |
| 摘 要： | 为使符号化模型检验技术适用于全部ω-正规性质,研究了ETL(extended temporal logic)的符号化模型检验方法.首先,扩展了LTL(linear temporal logic)的Tableau方法,给出了ETL的Tableau构造方法,进而给出了该方法基于BDD(binary decision diagram)的符号化实现.同时,在NuSMV的基础上实现了支持ETL符号化验证的模型检验工具ENuSMV.该工具允许用户自定义时序连接子,从而可以检验全部ω-正规性质.实验结果表明,ETL性质能够被高效地采用符号化技术加以检验.
|
| 关 键 词： | 符号化模型检验 扩展时序逻辑 Tableau方法 验证工具 ENuSMV |
| 修稿时间： | 2008/8/11 0:00:00 |
Symbolic Model Checking of ETL |
| |
| LIU Wan-Wei,WANG Ji and WANG Zhao-Fei.Symbolic Model Checking of ETL[J].Journal of Software,2009,20(8):2015-2025. |
| |
| Authors: | LIU Wan-Wei WANG Ji and WANG Zhao-Fei |
| |
| Affiliation: | National Laboratory for Parallel and Distributed Processing;School of Computer;National University of Defense Technology;Changsha 410073;China |
| |
| Abstract: | |
| |
| Keywords: | symbolic model checking ETL (extended temporal logic) tableau approach verification tool ENuSMV |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
