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 system...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 growth of cost.展开更多
A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are des...A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-order p-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.展开更多
Protocol formalization is one of a class of hard problems in testing routing protocols and characterized by dynamic, concurrent and distributed behavior. For the purpose of performing conformance testing of the open s...Protocol formalization is one of a class of hard problems in testing routing protocols and characterized by dynamic, concurrent and distributed behavior. For the purpose of performing conformance testing of the open shortest path first protocol link-state database (LSDB) synchronization process, the authors propose a formal model called global behavior tree, which describes global interactions among routers. The model is capable of representing distributed and concurrent behavior and allows for easy test derivation. The corresponding test notation and test derivation algorithm are studied. A simple test method is developed and a software tester is implemented. The results show that this model easily facilitates the testing process and allows a good test coverage.展开更多
Formal models of communicating and concurrent systems are one of the most important topics in formal methods,and process calculus is one of the most successful formal models of communicating and concurrent systems.In ...Formal models of communicating and concurrent systems are one of the most important topics in formal methods,and process calculus is one of the most successful formal models of communicating and concurrent systems.In the previous works,the author systematically studied topology in process calculus,probabilistic process calculus and pi-calculus with noisy channels in order to describe approximate behaviors of communicating and concurrent systems as well as randomness and noise in them.This article is a brief survey of these works.展开更多
文摘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 growth of cost.
基金Supported by the Intel Strategic CAD Labs, the National Natural Science Foundation of China （Grant No. 60421001）, and the Chinese Academy of Sciences.
文摘A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-order p-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.
基金the National Natural Science Foundation of China (No. 60102009 No. 90104002) and the National High-Tech Research and Development Program of China (No. 2001AA112061)
文摘Protocol formalization is one of a class of hard problems in testing routing protocols and characterized by dynamic, concurrent and distributed behavior. For the purpose of performing conformance testing of the open shortest path first protocol link-state database (LSDB) synchronization process, the authors propose a formal model called global behavior tree, which describes global interactions among routers. The model is capable of representing distributed and concurrent behavior and allows for easy test derivation. The corresponding test notation and test derivation algorithm are studied. A simple test method is developed and a software tester is implemented. The results show that this model easily facilitates the testing process and allows a good test coverage.
基金supported by the National Natural Science Foundation of China(Grant No.60621062).
文摘Formal models of communicating and concurrent systems are one of the most important topics in formal methods,and process calculus is one of the most successful formal models of communicating and concurrent systems.In the previous works,the author systematically studied topology in process calculus,probabilistic process calculus and pi-calculus with noisy channels in order to describe approximate behaviors of communicating and concurrent systems as well as randomness and noise in them.This article is a brief survey of these works.
