Nothing Special   »   [go: up one dir, main page]
Top > JACIII > An Efficient Specification for System Verification

single-jc.php

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

Paper:

Views over last 60 days: 630

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

Received:
November 11, 2005
Accepted:
February 8, 2006
Published:
November 20, 2006
Creative Commons License
Keywords:
formal verification, computation tree logic, temporal formula specification, strong/weak temporal order relation
Abstract
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:
C. Yamada, Y. Nagata, and Z. Nakao, “An Efficient Specification for System Verification,” J. Adv. Comput. Intell. Intell. Inform., Vol.10 No.6, pp. 931-938, 2006.
Data files:
References
  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, http://nusmv.irst.itc.it/
  13. [13] SMV, http://www.cs.cmu.edu/ 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.

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 Nov. 25, 2024