Abstract
We consider the problem of refinement checking for asynchronous processes where refinement corresponds to stutter-closed language inclusion. Since an efficient algorithmic solution to the refinement check demands the construction of a witness that defines the private specification variables in terms of the implementation variables, we first propose a construction to extract a synchronous witness from the specifi- cation. This automatically reduces individual refinement checks to reachability analysis. Second, to alleviate the state-explosion problem during search, we propose a reduction scheme that exploits the visibility information about transitions in a recursive manner based on the architectural hierarchy. Third, we establish compositional and assume-guarantee proof rules for decomposing the refinement check into subproblems. All these techniques work in synergy to reduce the computational requirements of refinement checking. We have integrated the proposed methodology based on an enumerative search in the model checker MOCHA. We illustrate our approach on sample benchmarks.
Note that stronger notions such as bisimulation and simulation are used in many process algebras, and are supported by automated tools [23],[7],14],[26].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.
M. Abadi and L. Lamport. Composing specifications. ACM TOPLAS, 15(1):73–132, 1993.
M. Abadi and L. Lamport. Conjoining specifications. ACM TOPLAS, 17:507–534, 1995.
R. Alur and T. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7–48, 1999.
R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In CAV’98: Computer Aided Verification, LNCS 1427, pp. 516–520, 1998.
R. Alur and B.-Y. Wang. “Next” heuristic for on-the-fly model checking. In CONCUR’99: Concurrency Theory, Tenth International Conference, LNCS 1664, pp. 98–113, 1999.
R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics-based tool for the verification of finite-state systems. ACM Trans. on Programming Languages and Systems, 15(1):36–72, 1993.
E. Emerson and A. Sistla. Symmetry and model checking. In CAV’93: Computer-Aided Verification, LNCS 697, pp. 463–478, 1993.
P. Godefroid. Using partial orders to improve automatic verification methods. In E. Clarke and R. Kurshan, editors, CAV’90: Computer-Aided Verification, LNCS 531, pp. 176–185, 1990.
O. Grümberg and D. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843–871, 1994.
T. Henzinger, X. Liu, S. Qadeer, and S. Rajamani. Formal specification and verification of a dataflow processor array. In ICCAD’99: International Conference on Computer-aided Design, pp. 494–499, 1999.
T. Henzinger, S. Qadeer, and S. Rajamani. You assume, we guarantee: Methodology and case studies. In CAV’98: Computer-aided Verification, LNCS 1427, pp. 521–525, 1998.
T. Henzinger, S. Qadeer, and S. Rajamani. Assume-guarantee refinement between different time scales. In CAV’99: Computer-aided Verification, LNCS 1633, pp. 208–221, 1999.
C. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
G. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279–295, 1997.
C. Ip and D. Dill. Verifying systems with replicated components in murφ. In Computer Aided Verification, LNCS 1102, 1996.
R. Kurshan. Computer-aided Verification of Coordinating Processes: the automatatheoretic approach. Princeton University Press, 1994.
N. Lynch. Distributed algorithms. Morgan Kaufmann, 1996.
N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Seventh ACM Symposium on Principles of Distributed Computing, pp. 137–151, 1987.
A. Martin. The design of a self-timed circuit for distributed mutual exclusion. In Chapel Hill Conference on Very Large Scale Integration, pp. 245–260, 1985.
K. McMillan. A compositional rule for hardware design refinement. In Computer-Aided Verification, LNCS 1254, pp. 24–35, 1997.
K. McMillan. Verification of an implementation of tomasulo’s algorithm by compositional model checking. In CAV’98: Computer-Aided Verification, LNCS 1427, pp. 110–121, 1998.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
D. Peled. Combining partial order reductions with on-the-fly model-checking. In CAV’94: Computer Aided Verification, LNCS 818, 1994.
A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In Current Trends in Concurrency, LNCS 224, pp. 510–584, 1986.
J. Scattergood. The semantics and implementation of machine-readable CSP. PhD thesis, Oxford University, 1998.
E. Stark. A proof technique for rely-guarantee properties. In Foundations of Software Technology and Theoretical Computer Science, LNCS 206, pp. 369–391, 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Grosu, R., Wang, BY. (2000). Automated Refinement Checking for Asynchronous Processes. In: Hunt, W.A., Johnson, S.D. (eds) Formal Methods in Computer-Aided Design. FMCAD 2000. Lecture Notes in Computer Science, vol 1954. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40922-X_5
Download citation
DOI: https://doi.org/10.1007/3-540-40922-X_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41219-9
Online ISBN: 978-3-540-40922-9
eBook Packages: Springer Book Archive