JACIII Vol.10 No.6 pp. 931-938
doi: 10.20965/jaciii.2006.p0931


An Efficient Specification 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

November 11, 2005
February 8, 2006
November 20, 2006
formal verification, computation tree logic, temporal formula specification, strong/weak temporal order relation

In design of complex and large scale systems, system verification has played an important role. In this article, we focus on specification process of model checking in system verifications. 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 specifications with temporal formulas are obtained inductively. We will show verification results using the proposed temporal formula specification method, and show that amount of memory, OBDD nodes, and execution time are reduced.

Cite this article as:
Chikatoshi Yamada, Yasunori Nagata, and Zensho Nakao, “An Efficient Specification for System Verification,” J. Adv. Comput. Intell. Intell. Inform., Vol.10, No.6, pp. 931-938, 2006.
Data files:
  1. [1] E. M. Clarke, O. Grumberg, and D. A. Peled, “Model Checking,” MIT Press, 2001.
  2. [2] L. Kenneth and L. McMillan, “Symbolic Model Checking,” Kluwer Academic Publishers, 1993.
  3. [3] M. Huth and M. Ryan, “Logic in Computer Science,” Cambridge University Press, 2001.
  4. [4] M. Dwyer, “Model Checking Software,” Springer, 2001.
  5. [5] T. Kropf, “Introduction to Formal Hardware Verification,” Springer, 1999.
  6. [6] B. Berard et al., “Systems and Software Verification,” Springer, 2001.
  7. [7] K. Strehl, “Symbolic Methods Applied to Formal Verification and Synthesis in Embedded Systems Design,” Shaker Verlag, 2000.
  8. [8] K. Schneider, “Verification of Reactive Systems – Formal Methods and Algorithms,” Springer, 2004.
  9. [9] R. E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Trans. On Computers, Vol.C-35, No.8, 1986.
  10. [10] T.-A. Chu, “Synthesis of self-timed VLSI circuits from graphtheoretic specifications,” Ph.D. thesis, MIT Laboratory for Computer Science, June, 1987.
  11. [11] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev, “Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers,” IEICE Transactions on Information and Systems, Vol.E80-D, No.3, pp. 315-325, 1997.
  12. [12] NuMSV,
  13. [13] SMV, modelcheck/
  14. [14] H. Hiraishi, “Yet Another Image Computation for Symbolic Model Verifier SMV,” IEICE Trans. D-I, Vol.J82-D-I, No.7 pp. 791-798, 1999.
  15. [15] T. Tsuchiya, S. Nagano, R. Bt Paidi, and T. Kikuno, “Symbolic Model Checking for Self-Stabilizing Algorithms,” IEEE Trans. Parallel and Distributed Systems, Vol.12, No.6, 2001.

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

Last updated on Mar. 05, 2021