Simulation refinement for concurrency verification |
| |
Authors: | Wim H. Hesselink |
| |
Affiliation: | Department of Computing Science, University of Groningen, P.O. Box 407, 9700 AK Groningen, The Netherlands |
| |
Abstract: | In recent years, we applied and extended the theory of Abadi and Lamport (1991) [1] on the existence of refinement mappings. The present paper presents an overview of our extensions of the theory. For most concepts we provide examples or pointers to case studies where they occurred. The paper presents the results on semantic completeness. It sketches out how the theory is related to the other formalisms in the area. It discusses the tension between semantic completeness and methodological convenience. It concludes with our experience with the theorem provers NQTHM and PVS that were used during these projects. |
| |
Keywords: | Refinement Simulation Atomicity Verification Semantic completeness |
本文献已被 ScienceDirect 等数据库收录! |