摘要
针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展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.
出处
《华南理工大学学报（自然科学版）》
EI
CAS
CSCD
北大核心
2011年第7期163-168,共6页
Journal of South China University of Technology(Natural Science Edition)
基金
国家"863"计划项目(2007AA010408)
国家自然科学基金青年基金资助项目(60901078
61003079)
高等学校博士学科点专项科研基金资助项目(新教师类)(20100203120012)
