欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
为使符号化模型检验技术适用于全部ω-正规性质，研究了ETL（extended temporal logic）的符号化模型检验方法．首先，扩展了LTL（linear temporal logic）的Tableau方法，给出了ETL的Tableau构造方法，进而给出了该方法基于BDD（binary decision diagram）的符号化实现同时，在NuSMV的基础上实现了支持ETL符号化验证的模型检验工具ENusMV该工具允许用户自定义时序连接子，从而可以检验全部ω-正规性质．实验结果表明，ETL性质能够被高效地采用符号化技术加以检验．
英文摘要：
To make symbolic model checking approach applicable to all o-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 o-regular properties can be verified. Experimental results show that ETL can also be efficiently verified by the symbolic approach.
同期刊论文项目
同项目期刊论文
期刊信息
位置：