• Articles • 上一篇    下一篇

Automatic and Hierarchical Verification for Concurrent Systems

赵旭东; 冯玉琳;   

  1. University of Science and Technology of China;
  • 出版日期:1990-05-10 发布日期:1990-05-10

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 ...

关键词: test correlation, scan architecture design, scan-based testing, test data compression

Abstract: 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] . 利用测试中的相关性实现低成本扫描测试[J]. , 2007, 22(5): 681-694 .
[2] . [J]. , 2005, 20(2): 210-215.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持:support@magtech.com.cn
总访问量: