• Articles • Previous Articles     Next Articles

Automatic and Hierarchical Verification for Concurrent Systems

Zhao Xudong; Feng Yulin;   

  1. University of Science and Technology of China;
  • Online:1990-05-10 Published:1990-05-10

Proving correctness of concurrent systems is quite difficult because of the high level of nondeterminism,especially in large and complex ones.AMC is a model checking system for verifying asynchronous concurrent systems by using branching time temporal logic.This paper introduces the tech- niques of the modelling approach,especially how to construct models for large concurrent systems with the concept of hierarchy,which has been proved to be effective and practical in verifying large systems without a large ...

Key words: scan-based testing; test data compression; test correlation; scan architecture design;

[1] M.Ben-Ari, A.Pnueli, and Z.Manna, The temporal logic of branching time, Acta Inf., 20:3 (1983),207-226.

[2] M.C.Browne, E.M.Clerke, D.L.Dill, and B.Mishra, Automatic verification of sequential circults using temporal logic., IEEE Trans.Computers, C-35:12 (1986), 1035-1044.

[3] E.M.Clarke, E.A.Emerson, and A.P.Sistla, Automatic verification of finite-state concurrent systems using temporal logic specification, ACM Trans.Program Lang.Syst., 8:2 (1986), 244-263.

[4] E.A.Emerson, and J.Y.Halpern, "Sometimes" and "not never" revisited:on branching versus linear time temporal logic. J. ACM, 33:1 (1986),151-178

[5] Feng Yulin, Lin Huimin and C.S.Tang, A proof system for temporal logic programs. Computer Research and Development, 22:10 (1985) (in Chinese) ……….
[1] Ozgur Sinanoglu, Mohammed Al-Mulla, Noora A. Shunaiber, and Alex Orailoglu, Member, IEEE. Scan Cell Positioning for Boosting the Compression of Fan-Out Networks [J]. , 2009, 24(5): 939-948.
[2] Ozgur Sinanoglu. Low Cost Scan Test by Test Correlation Utilization [J]. , 2007, 22(5): 681-694 .
[3] Terumine Hayashi, Haruna Yoshioka, Tsuyoshi Shinogi, Hidehiko Kita, and Haruhiko Takase. On Test Data Compression Using Selective Don t-Care Identification [J]. , 2005, 20(2): 210-215.
Full text



No Suggested Reading articles found!

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved