An Efficient Temporal Formula Specification Method for Asynchronous Concurrent Systems

Design verification has played an important role in the design of large scale and complex systems. System verification ascertains whether designed systems can be executed or specified. Symbolic model checker SMV is widely-used for the verification. In this article, we focus on specification process of model checking for the SMV. Behaviors of modeled systems are in general specified by temporal formulas of computation tree logic, and users must know well about temporal specification because the specification might be complex. We propose a method by which temporal formulas are obtained inductively, and amounts of memory, OBDD nodes, and execution time are reduced. We will show verification results using the proposed a temporal formula specification method by some benchmark examples.