Skip to main content
SpringerLink
Log in

Automatic and hierarchical verification for concurrent systems

  • Regular Papers
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

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 techniques 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 growth of cost.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  Google Scholar 

  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.

    Article  MATH  Google Scholar 

  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.

    Article  MATH  MathSciNet  Google Scholar 

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

  6. Y. Feng, X. Zhao and D. Guo, Automatic verification of concurrent systems using temporal logic, Chinese.J. of Computers,13: 2 (1990).

    Google Scholar 

  7. D. Lehmann, A. Pnueli and J. Stavi, Impartiality, justice and fairness: The ethics of concurrent termination, In Automata, Languages and programming, Lecture Notes in Computer Science 115, Springer-Verlag, New York, 1981, 265–277.

    Google Scholar 

  8. B. Mishra and E. M. Clerke, Hierarchical verification of asynchronous circuits using temporal logic,Theoretical Computer Science,38 (1985), 269–291.

    Article  MATH  MathSciNet  Google Scholar 

  9. Zhao Xudong, Automatic and hierarchical verification for asynchronous concurrent systems, CS Thesis, USTC, Spring, 1988.

Download references

Author information

Authors and Affiliations

  1. University of Science and Technology of China, China

    Zhao Xudong & Feng Yulin

Authors
  1. Zhao Xudong
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Feng Yulin
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Zhao, X., Feng, Y. Automatic and hierarchical verification for concurrent systems. J. of Comput. Sci. & Technol. 5, 241–249 (1990). https://doi.org/10.1007/BF02945312

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02945312

Keywords

Search

Navigation