作者：朱维军 周清雷 张海宾模型检测扩展tempura语言区间时序逻辑区间模型程序规范统一框架
摘要：针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间时序逻辑统一模型检测算法,以判定由上述定义的语言子集所书写的规范程序是否满足命题版扩展区间时序逻辑公式所描述的性质.具体方法是首先翻译规范程序到命题扩展区间时序逻辑公式,然后使用该逻辑的公式满足性判定算法进行自动验证.验证实例证实了新方法的有效性.
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
《华南理工大学学报·社会科学版》（CN：44-1443/C）是一本有较高学术价值的大型双月刊，自创刊以来，选题新奇而不失报道广度，服务大众而不失理论高度。颇受业界和广大读者的关注和好评。 《华南理工大学学报·社会科学版》自创刊以来，本刊坚持以马克思列宁主义、思想、邓小平理论、"三个代表"重要思想、科学发展观、新时代中国特色社会主义思想为指导，立足广东，面向全国，积极反映人文社会科学各领域在改革开放和现代化建设中理论与实践的成果，努力把本刊办成有特色、有水平、有影响的综合性学术期刊和重要理论研究阵地。
杂志详情
