Journal of South China University of Technology (Natural Science Edition) ›› 2011, Vol. 39 ›› Issue (7): 163-168.doi: 10.3969/j.issn.1000-565X.2011.07.027

• Computer Science & Technology • Previous Articles    

Model Checking Algorithm of Extended Tempura Language in Unified Logical Framework

Zhu Wei-jun1  Zhou Qing-lei1  Zhang Hai-bin2   

  1. 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
  • Received:2010-11-30 Online:2011-07-25 Published:2011-06-03
  • Contact: 朱维军(1976-) ，男，博士，讲师，主要从事计算机形式化方法、高可信软件研究． E-mail:zhuweijun76@163.com
  • About author:朱维军(1976-) ，男，博士，讲师，主要从事计算机形式化方法、高可信软件研究．
  • Supported by:

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

PDF

836

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 checking 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 property. Case study indicates that the proposed algorithm is effective.

Key words: model checking, extended Tempura language, interval temporal logic, interval model, program specification, unified framework