Advertisement

Automated Refinement Checking for Asynchronous Processes

  • Rajeev Alur
  • Radu Grosu
  • Bow-Yaw Wang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

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.

Keywords

Model Check Proof Obligation Leader Election Proof Rule Private Variable 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    M. Abadi and L. Lamport. Composing specifications. ACM TOPLAS, 15(1):73–132, 1993.CrossRefGoogle Scholar
  3. 3.
    M. Abadi and L. Lamport. Conjoining specifications. ACM TOPLAS, 17:507–534, 1995.CrossRefGoogle Scholar
  4. 4.
    R. Alur and T. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7–48, 1999.CrossRefMathSciNetGoogle Scholar
  5. 5.
    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.CrossRefGoogle Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    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.CrossRefGoogle Scholar
  8. 8.
    E. Emerson and A. Sistla. Symmetry and model checking. In CAV’93: Computer-Aided Verification, LNCS 697, pp. 463–478, 1993.Google Scholar
  9. 9.
    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.CrossRefGoogle Scholar
  10. 10.
    O. Grümberg and D. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843–871, 1994.CrossRefGoogle Scholar
  11. 11.
    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.Google Scholar
  12. 12.
    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.Google Scholar
  13. 13.
    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.CrossRefGoogle Scholar
  14. 14.
    C. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  15. 15.
    G. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279–295, 1997.CrossRefMathSciNetGoogle Scholar
  16. 16.
    C. Ip and D. Dill. Verifying systems with replicated components in murφ. In Computer Aided Verification, LNCS 1102, 1996.Google Scholar
  17. 17.
    R. Kurshan. Computer-aided Verification of Coordinating Processes: the automatatheoretic approach. Princeton University Press, 1994.Google Scholar
  18. 18.
    N. Lynch. Distributed algorithms. Morgan Kaufmann, 1996.Google Scholar
  19. 19.
    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.Google Scholar
  20. 20.
    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.Google Scholar
  21. 21.
    K. McMillan. A compositional rule for hardware design refinement. In Computer-Aided Verification, LNCS 1254, pp. 24–35, 1997.Google Scholar
  22. 22.
    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.CrossRefGoogle Scholar
  23. 23.
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  24. 24.
    D. Peled. Combining partial order reductions with on-the-fly model-checking. In CAV’94: Computer Aided Verification, LNCS 818, 1994.Google Scholar
  25. 25.
    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.CrossRefGoogle Scholar
  26. 26.
    J. Scattergood. The semantics and implementation of machine-readable CSP. PhD thesis, Oxford University, 1998.Google Scholar
  27. 27.
    E. Stark. A proof technique for rely-guarantee properties. In Foundations of Software Technology and Theoretical Computer Science, LNCS 206, pp. 369–391, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Rajeev Alur
    • 1
  • Radu Grosu
    • 1
  • Bow-Yaw Wang
    • 1
  1. 1.Department of Computer and Information ScienceUniversity of PennsylvaniaPhiladelphia

Personalised recommendations