In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is loca...In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is local in that it generates and investigates thereachable state space in top-down fashion and maintains the partition for time evaluations as coarseas possible while on-the-fly instantiating data variables. It can deal with not only data variableswith finite value domain, but also the so called data independent variables with infinite valuedomain. To authors knowledge, this is the first algorithm for model checking timed systemscontaining value-passing features.展开更多
A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown...A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.展开更多
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.展开更多
文摘In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is local in that it generates and investigates thereachable state space in top-down fashion and maintains the partition for time evaluations as coarseas possible while on-the-fly instantiating data variables. It can deal with not only data variableswith finite value domain, but also the so called data independent variables with infinite valuedomain. To authors knowledge, this is the first algorithm for model checking timed systemscontaining value-passing features.
基金This work was partially supported by the National Natural Science Foundationof China (Grant No. 69833020) the National High Technology Development Program of China (Grant No. 2002AA144050)the National Grand Fundamental Research 973 Program of China
文摘A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.
基金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.
