| 摘要: |
| 为使符号化模型检验技术适用于全部ω-正规性质,研究了ETL(extended temporal logic)的符号化模型检验方法.首先,扩展了LTL(linear temporal logic)的Tableau方法,给出了ETL的Tableau构造方法,进而给出了该方法基于BDD(binary decision diagram)的符号化实现.同时,在NuSMV的基础上实现了支持ETL符号化验证的模型检验工具ENuSMV.该工具允许用户自定义时序连接子,从而可以检验全部ω-正规性质.实验结果表明,ETL性质能够被高效地采用符号化技术加以检验. |
| 关键词: 符号化模型检验 扩展时序逻辑 Tableau方法 验证工具 ENuSMV |
| DOI： |
| 分类号: |
| 基金项目: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)) |
|
| Symbolic Model Checking of ETL |
|
LIU Wan-Wei,WANG Ji,WANG Zhao-Fei
|
| 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. |
| Key words: symbolic model checking ETL (extended temporal logic) tableau approach verification tool ENuSMV |
