single-jc.php

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

Paper:

Views over last 60 days: 451

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, 2004
Accepted:
December 25, 2004
Published:
May 20, 2005
Creative Commons License
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:

Creative Commons License  This article is published under a Creative Commons Attribution-NoDerivatives 4.0 Internationa License.

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

Last updated on Jan. 31, 2023