Skip to main content
SpringerLink
Log in

“Next” Heuristic for On-the-Fly Model Checking

  • Conference paper
  • First Online:
CONCUR’99 Concurrency Theory (CONCUR 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1664))

Included in the following conference series:

Abstract

We present a new heuristic for on-the-fly enumerative invariant verification. The heuristic is based on a construct for temporal scaling, called next, that compresses a sequence of transitions leading to a given target set into a single metatransition. First, we give an on-the-fly algorithm to search a process expression built using the constructs of hiding, parallel composition, and temporal scaling. Second, we show that as long the target set Θ of transitions includes all transitions that access variables shared with the environment, the process next Θ for P and P are equivalent according to the weak-simulation equivalence. As a result, to search the product of given processes, we can cluster processes into groups with as little communication among them as possible, and compose the groups only after applying appropriate hiding and temporal scaling operators. Applying this process recursively gives an expression that has multiple nested applications of next, and has potentially much fewer states than the original product. We report on an implementation, and show significant reductions for a tree-structured parity computer and a ring-structured leader-election protocol.

Supported in part by NSF CAREER award CCR-9734115 and by the DARPA grant NAG2-1214.

Supported by the DARPA grant NAG2-1214.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur and T. A. Henzinger. Reactive modules. In Proceedings of the 11th IEEE Symposium on Logic in Computer Science, pages 207–218, 1996.

    Google Scholar 

  2. R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In Proceedings of the 10th International Conference on Computer Aided Verification, LNCS 1427, pages 516–520. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  3. R. Alur, T. Henzinger, and S. Rajamani. Symbolic exploration of transition hierarchies. In Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1384, pages 330–344. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  4. A. Bouajjani, J. C. Fernandez, and N. Halbwachs. Minimal model generation. In Computer-Aided Verification, 2nd International Conference, CAV’90, LNCS 531, pages 197–203. Springer-Verlag, 1990.

    Chapter  Google Scholar 

  5. G. Berry and G. Gonthier. The synchronous programming language esterel: design, semantics, implementation. Technical Report 842, INRIA, 1988.

    Google Scholar 

  6. G. Boudol, V. Roy, R. de Simone, and D. Vergamini. Process calculi, from theory to practice: verification tools. In Automatic Verification Methods for Finite State Systems, LNCS 407, pages 1–10. 1987.

    Google Scholar 

  7. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, LNCS 131, pages 52–71. Springer-Verlag, 1981.

    Chapter  Google Scholar 

  8. E. M. Clarke, T. Filkorn, and S. Jha. Exploiting symmetry in temporal-logic model checking. In Computer-Aided Verification, Fifth International Conference, CAV’95, LNCS 697, pages 450–462. Springer-Verlag, 1993.

    Google Scholar 

  9. E. M. Clarke and R. P. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6):61–67, 1996.

    Article  Google Scholar 

  10. 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.

    Article  Google Scholar 

  11. D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522–525, 1992.

    Google Scholar 

  12. E. A. Emerson and A. P. Sistla. Symmetry and model checking. In Computer-Aided Verification, Fifth International Conference, CAV’95, LNCS 697, pages 463–478. Springer-Verlag, 1993.

    Google Scholar 

  13. J. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A protocol validation and verification toolbox. In Proceedings of the Eighth International Conference on Computer-Aided Verification, LNCS 1102. SpringerVerlag, 1996.

    Google Scholar 

  14. P. Godefroid. Using partial orders to improve automatic verification methods. In E. M. Clarke and R. P. Kurshan, editors, Computer-Aided Verification, 2nd International Conference, CAV’90, LNCS 531, pages 176–185. Springer-Verlag, 1990.

    Chapter  Google Scholar 

  15. N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer Academic Publishers, 1993.

    Google Scholar 

  16. G. J. Holzmann. The model checker spin. IEEE Trans. on Software Engineering, 23(5):279–295, 1997.

    Article  MathSciNet  Google Scholar 

  17. C. N. Ip and D. L. Dill. Verifying systems with replicated components in mur’. In Proceedings of the Eighth International Conference on Computer Aided Verification, LNCS 1102. Springer-Verlag, 1996.

    Google Scholar 

  18. J.-P. Krimm and L. Mounier. Compositional state space generation of lotos programs. 1997.

    Google Scholar 

  19. P. Kanellakis and S. A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation, 86(1):43–68, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  20. N. A. Lynch. Distributed algorithms. Morgan Kaufmann, 1996.

    Google Scholar 

  21. R. Milner. A Calculus of Communicating Systems. LNCS 92. Springer-Verlag, 1980.

    MATH  Google Scholar 

  22. D. Peled. Combining partial order reductions with on-the-fly model-checking. In Computer Aided Verification, Proc. 6th Int. Conference, LNCS 818. SpringerVerlag, 1994.

    Google Scholar 

  23. R. Paige and R. E. Tarjan. Three partition-refinement algorithms. SIAM Journal on Computing, 16(6):973–989, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  24. J. P. Queille and J. Sifakis. Specification and verification of concurrent programs in CESAR. In Proceedings of the Fifth International Symposium on Programming, LNCS 137, pages 195–220. Springer-Verlag, 1982.

    Google Scholar 

  25. A. Valmari. A stubborn attack on state explosion. Formal Methods in System Design, 1:297–322, 1992.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer and Information Science, University of Pennsylvania, Pennsylvania

    Rajeev Alur & Bow-Yaw Wang

  2. Bell Laboratories, Lucent Technologies, USA

    Rajeev Alur

Authors
  1. Rajeev Alur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bow-Yaw Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing Science, Eindhoven University of Technology, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    Jos C. M. Baeten  & Sjouke Mauw  & 

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alur, R., Wang, BY. (1999). “Next” Heuristic for On-the-Fly Model Checking. In: Baeten, J.C.M., Mauw, S. (eds) CONCUR’99 Concurrency Theory. CONCUR 1999. Lecture Notes in Computer Science, vol 1664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48320-9_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-48320-9_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66425-3

  • Online ISBN: 978-3-540-48320-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation