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

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