Abstract: Formal verification of temporal logic programs plays an important role in improving program correctness. A framing projection temporal logic language, called Framed Tempura, is the research object as an executable subset of projection temporal logic. Propositional temporal logic was used to describe properties of a Framed Tempura program,thus the program p and properties ф were both formalized in projection temporal logic, then model checking needs to eva luate whether or not p→ф is valid which can be translated into evaluate whether or not p∧乛ф is unsatisfiablc, and this problem is solved by constructing the normal form graph of p∧乛ф. At last, an example of model checking a F ramed (hempura program was given.

Key words: Temporal logic programs,Formal verification,Normal form graphs,Model checking