JACIII Vol.9 No.3 pp. 321-328
doi: 10.20965/jaciii.2005.p0321


Inductive Temporal Formula Specifications for System Verification

Chikatoshi Yamada*, Yasunori Nagata**, and Zensho Nakao**

*Takushoku University Hokkaido College, 4558 Memu, Fukagawa, Hokkaido 074-8585, Japan

**Department of Electrical and Electronics Engineering, University of the Ryukyus, 1 Senbaru, Nishihara, Nakagami, Okinawa 903-0213, Japan

October 31, 2004
December 25, 2004
May 20, 2005
inductive specification, strong/weak temporal order relation, computation tree logic, system verification
Design verification has played an important role in the design of large scale and complex systems. In this article, we focus on model checking methods. 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 temporal formulas are obtained inductively, and amounts of memory and time are reduced. We will show verification results using the proposed method.
Cite this article as:
C. Yamada, Y. Nagata, and Z. Nakao, “Inductive Temporal Formula Specifications for System Verification,” J. Adv. Comput. Intell. Intell. Inform., Vol.9 No.3, pp. 321-328, 2005.
Data files:

*This site is desgined based on HTML5 and CSS3 for modern browsers, e.g. Chrome, Firefox, Safari, Edge, Opera.

Last updated on May. 10, 2024