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

摘要：

针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间时序逻辑统一模型检测算法,以判定由上述定义的语言子集所书写的规范程序是否满足命题版扩展区间时序逻辑公式所描述的性质.具体方法是首先翻译规范程序到命题扩展区间时序逻辑公式,然后使用该逻辑的公式满足性判定算法进行自动验证.验证实例证实了新方法的有效性.

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

所属期刊栏目：39

分类号：TP301(计算技术、计算机技术)

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

在线出版日期：2011-12-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：163-168