| 扩展Tempura语言统一模型检测算法 |
| |
| 引用本文： | 朱维军,周清雷,张海宾.扩展Tempura语言统一模型检测算法[J].华南理工大学学报(自然科学版),2011,39(7):163-168. |
| |
| 作者姓名： | 朱维军 周清雷 张海宾 |
| |
| 作者单位： | 1. 郑州大学信息工程学院,河南郑州,450001
2. 西安电子科技大学计算机学院,陕西西安,710071 |
| |
| 基金项目： | 国家“863”计划项目(2007AA010408); 国家自然科学基金青年基金资助项目(60901078,61003079); 高等学校博士学科点专项科研基金资助项目(新教师类)(20100203120012) |
| |
| 摘 要： | 针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间时序逻辑统一模型检测算法,以判定由上述定义的语言子集所书写的规范程序是否满足命题版扩展区间时序...
|
| 关 键 词： | 模型检测 扩展Tempura语言 区间时序逻辑 区间模型 程序规范 统一框架 |
Model Checking Algorithm of Extended Tempura Language in Unified Logical Framework |
| |
| Zhu Wei-jun,Zhou Qing-lei,Zhang Hai-bin.Model Checking Algorithm of Extended Tempura Language in Unified Logical Framework[J].Journal of South China University of Technology(Natural Science Edition),2011,39(7):163-168. |
| |
| Authors: | Zhu Wei-jun Zhou Qing-lei Zhang Hai-bin |
| |
| Institution: | Zhu Wei-jun1 Zhou Qing-lei1 Zhang Hai-bin2 (1.School of Information Engineering,Zhengzhou University,Zhengzhou 450001,Henan,China,2.School of Computer Science and Technology,Xidian University,Xi'an 710071,Shaanxi,China) |
| |
| Abstract: | 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 algo... |
| |
| Keywords: | model checking extended Tempura language interval temporal logic interval model program specification unified framework |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
