Paper:
Views over last 60 days: 479
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
Received:October 31, 2004Accepted:December 25, 2004Published:May 20, 2005
Keywords:inductive specification, strong/weak temporal order relation, computation tree logic, system verification
Abstract
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:
