ETL的符号化模型检验

作者：刘万伟; 王戟; 王昭飞

来源：软件学报, 2009, (08): 2015-2025.

• 符号化模型检验
• 扩展时序逻辑
• Tableau方法
• 验证工具
• ENuSMV symbolic model checking
• ETL (extended temporal logic)
• tableau approach
• verification tool
• ENuSMV

为使符号化模型检验技术适用于全部ω-正规性质,研究了ETL(extended temporal logic)的符号化模型检验方法.首先,扩展了LTL(linear temporal logic)的Tableau方法,给出了ETL的Tableau构造方法,进而给出了该方法基于BDD(binary decision diagram)的符号化实现.同时,在NuSMV的基础上实现了支持ETL符号化验证的模型检验工具ENuSMV.该工具允许用户自定义时序连接子,从而可以检验全部ω-正规性质.实验结果表明,ETL性质能够被高效地采用符号化技术加以检验.

• 单位
  中国人民解放军国防科学技术大学