扩展Tempura语言统一模型检测算法  

Model Checking Algorithm of Extended Tempura Language in Unified Logical Framework

作　　者：朱维军[1] 周清雷[1] 张海宾[2] 

机构地区：[1]郑州大学信息工程学院,河南郑州450001 [2]西安电子科技大学计算机学院,陕西西安710071

出　　处：《华南理工大学学报（自然科学版）》2011年第7期163-168,共6页Journal of South China University of Technology(Natural Science Edition)

基　　金：国家"863"计划项目(2007AA010408);国家自然科学基金青年基金资助项目(60901078;61003079);高等学校博士学科点专项科研基金资助项目(新教师类)(20100203120012)

摘　　要：针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间时序逻辑统一模型检测算法,以判定由上述定义的语言子集所书写的规范程序是否满足命题版扩展区间时序逻辑公式所描述的性质.具体方法是首先翻译规范程序到命题扩展区间时序逻辑公式,然后使用该逻辑的公式满足性判定算法进行自动验证.验证实例证实了新方法的有效性.In order to find a unified model checking algorithm for extended interval temporal logic（EITL）,the decidable subset of extended Tempura language,which is an executable subset of EITL,is obtained by defining that the constants and the variables in the first-order extended Tempura are all in a finite enumerable type and by combining the constraint version of the first-order extended Tempura with propositional EITL.Then,a novel model che-cking algorithm of EITL in unified logical framework is proposed.The algorithm is used to decide whether a specification program written in the decidable subset of extended Tempura language satisfies the property described as a propositional EITL formula,and the check includes two steps： to translate the specification program into a propositional EITL formula and to use the existing EITL satisfiability-checking algorithms to automatically check the pro-perty.Case study indicates that the proposed algorithm is effective.

关 键 词：模型检测 扩展Tempura语言 区间时序逻辑 区间模型 程序规范 统一框架 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]