The sweep-line state space exploration method. (English) Zbl 1238.68085
Summary: The sweep-line method exploits intrinsic progress in concurrent systems to alleviate the state explosion problem in explicit state model checking. The concept of progress makes it possible to delete states from the memory during state space exploration and thereby reduce peak memory usage. The contribution of this paper is twofold. First, we provide a coherent presentation of the sweep-line theory and the many variants of the method that have been developed over the past 10 years since the basic idea of the method was conceived. Second, we survey a selection of case studies where the sweep-line method has been put into practical use for the verification of concurrent systems.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Keywords:
explicit state space exploration; model checking; concurrent systems; verification; state explosion; sweep-line method; coloured Petri netsReferences:
| [1] | Baier, C.; Katoen, J.-P., Principles of Model Checking (2008), MIT Press · Zbl 1179.68076 |
| [2] | Clarke, E.; Grumberg, O.; Peled, D., Model Checking (1999), The MIT Press |
| [3] | Clarke, E.; Emerson, E.; Sifakis, J., Turing lecture: model checking-algorithmic verification and debugging, Communications of the ACM, 52, 74-84 (2009) |
| [4] | Emerson, E. A., (Temporal and Modal Logic. Temporal and Modal Logic, Handbook of Theoretical Computer Science, vol. B (1990), Elsevier), 995-1072, (chapter 16) · Zbl 0900.03030 |
| [5] | Reisig, W., (Petri Nets — An Introduction. Petri Nets — An Introduction, EATCS Monographs on Theoretical Computer Science, vol. 4 (1985), Springer) · Zbl 0555.68033 |
| [6] | Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall · Zbl 0637.68007 |
| [7] | Alur, R.; Dill, D., A Theory of Timed Automata, TCS, 126, 2, 183-235 (1994) · Zbl 0803.68071 |
| [8] | Holzmann, G. J., The SPIN Model Checker (2003), Addison-Wesley |
| [9] | Barnat, J.; Brim, L.; Černá, I.; Moravec, P.; Ročkai, P.; Šimeček, P., DiVinE — A Tool for Distributed Verification, (CAV. CAV, LNCS, vol. 4144 (2006), Springer), 278-281 |
| [10] | Ratzer, Cpn tools for editing, simulating, and analysing coloured petri nets, (ICATPN. ICATPN, LNCS, vol. 2679 (2003), Springer), 450-462 |
| [11] | McMillan, K., Symbolic Model Checking (1993), Kluwer · Zbl 0784.68004 |
| [12] | Biere, A.; Cimatti, A.; Clarke, E.; Fujita, M.; Zhu, Y., Symbolic model checking using SAT procedures instead of BDDs, (DAC (1999)), 317-320 |
| [13] | Esparza, J.; Römer, S.; Vogler, W., An improvement of McMillan’s unfolding algorithm, Formal Methods in System Design, 20, 3, 285-310 (2002) · Zbl 1017.68085 |
| [14] | Valmari, A., The state explosion problem, (Lectures on Petri Nets I: Basic Models. Lectures on Petri Nets I: Basic Models, LNCS, vol. 1491 (1998), Springer), 429-528 · Zbl 0903.00072 |
| [15] | Clarke, E. M.; Grumberg, O.; Minea, M.; Peled, D., State space reduction using partial order techniques, STTT, 2, 3, 279-287 (1999) · Zbl 1065.68506 |
| [16] | Westergaard, M., The ComBack method-extending hash compaction with backtracking, (ICATPN. ICATPN, LNCS, vol. 4546 (2007), Springer), 445-464 · Zbl 1226.68066 |
| [17] | Holzmann, G., An analysis of bitstate hashing, Formal Methods in System Design, 13, 289-307 (1998) |
| [18] | Stern, U.; Dill, D., Improved probabilistic verification by hash compaction, (CHARME. CHARME, LNCS, vol. 987 (1995), Springer), 206-224 |
| [19] | Clarke, E.; Emerson, E.; Jha, S.; Sistla, A. P., Symmetry reductions in model checking, (CAV. CAV, LNCS, vol. 1427 (1998), Springer), 147-158 |
| [20] | Jensen, K., Condensed state spaces for symmetrical coloured petri nets, Formal Methods in System Design, 9, 1/2, 7-40 (1996) |
| [21] | Stern, U.; Dill, D., Using magnetic disk instead of main memory in the Murphi verifier, (CAV. CAV, LNCS, vol. 1427 (1998), Springer), 172-183 |
| [22] | Godefroid, P.; Holzmann, G. J.; Pirottin, D., State-space caching revisited, Formal Methods in System Design, 7, 3, 227-241 (1995) |
| [23] | Behrmann, G.; Larsen, K.; Pelnek, R., To store or not to store, (CAV. CAV, LNCS, vol. 2725 (2003), Springer), 433-445 · Zbl 1278.68155 |
| [24] | Christensen, S.; Kristensen, L.; Mailund, T., A sweep-line method for state space exploration, (TACAS. TACAS, LNCS, Vol. 2031 (2001), Springer), 450-464 · Zbl 0978.68547 |
| [25] | Kristensen, L.; Mailund, T., A generalised sweep-line method for safety properties, (FME. FME, LNCS, vol. 2391 (2002), Springer), 549-567 · Zbl 1064.68553 |
| [26] | Mailund, T.; Westergaard, M., Obtaining memory-efficient reachability graph representations using the sweep-line method, (TACAS. TACAS, LNCS, vol. 2988 (2004), Springer), 177-191 · Zbl 1126.68506 |
| [27] | Kristensen, L.; Mailund, T., Efficient path finding with the sweep-line method using external storage, (ICFEM. ICFEM, LNCS, vol. 2885 (2003), Springer), 319-337 |
| [28] | Billington, J.; Gallasch, G.; Kristensen, L.; Mailund, T., Exploiting equivalence reduction and the sweep-line method for detecting terminal states, IEEE Transactions on SMC — Part A, 34, 1, 23-38 (2004) |
| [29] | Gallasch, G. E.; Billington, J.; Vanit-Anunchai, S.; Kristensen, L., Checking safety properties on-the-fly with the sweep-line method, STTT, 9, 3-4, 371-392 (2007) |
| [30] | Westergaard, M.; Evangelista, S.; Kristensen, L., ASAP: an extensible platform for state space analysis, (ICATPN. ICATPN, LNCS, vol. 5606 (2009), Springer), 303-312 |
| [31] | Schmidt, K., LoLA: a low level analyser, (ICATPN. ICATPN, LNCS, vol. 1825 (2000), Springer), 465-474 · Zbl 0986.68684 |
| [32] | Gordon, S.; Kristensen, L.; Billington, J., Verification of a revised WAP wireless transaction protocol, (ICATPN. ICATPN, LNCS, vol. 2360 (2002), Springer), 182-202 · Zbl 1047.68508 |
| [33] | Vanit-Anunchai, S.; Billington, J.; Gallasch, G. E., Analysis of the datagram congestion control protocols connection management procedures using the sweep-line method, STTT, 10, 1, 29-56 (2008) |
| [34] | Gallasch, G.; Ouyang, C.; Billington, J.; Kristensen, L., Experimenting with progress mappings for the sweep-line analysis of the internet open trading protocol, (CPN (2004)), 19-38 |
| [35] | Gallasch, G. E.; Han, B.; Billington, J., Sweep-Line analysis of TCP connection management, (ICFEM. ICFEM, LNCS, vol. 3785 (2005), Springer), 156-172 |
| [36] | Jensen, K.; Kristensen, L., Coloured Petri Nets — Modelling and Validation of Concurrent Systems, Monograph (2009), Springer · Zbl 1215.68153 |
| [37] | Kristensen, L.; Mailund, T., A compositional sweep-line state space exploration method, (FORTE. FORTE, LNCS, vol. 2529 (2002), Springer), 327-343 · Zbl 1037.68515 |
| [38] | Mailund, T., Analysing infinite-state systems by combining equivalence reduction and the sweep-line method, (ICATPN. ICATPN, LNCS, Vol. 2360 (2002), Springer), 314-333 · Zbl 1047.68609 |
| [39] | T. Mailund, Sweeping the state space a sweep-line state space exploration method, Ph.D. Thesis, Computer Science Department, University of Aarhus, 2003.; T. Mailund, Sweeping the state space a sweep-line state space exploration method, Ph.D. Thesis, Computer Science Department, University of Aarhus, 2003. |
| [40] | Kristensen, L. M.; Jørgensen, J. B.; Jensen, K., Application of Coloured Petri Nets in System Development, (Proc. of 4th Advanced Course on Petri Nets. Proc. of 4th Advanced Course on Petri Nets, LNCS, Vol. 3098 (2004), Springer), 626-685 · Zbl 1088.68664 |
| [41] | Schmidt, K., Automated generation of a progress measure for the sweep-line method, (TACAS. TACAS, LNCS, vol. 2988 (2004), Springer), 192-204 · Zbl 1126.68511 |
| [42] | Valmari, A., A stubborn attack on state explosion, (Proc. of CAV’90. Proc. of CAV’90, LNCS, vol. 531 (1990), Springer), 156-165 · Zbl 0765.68147 |
| [43] | Mitchell, B.; Kristensen, L. M.; Zhang, L., Formal specification and state space analysis of an operational planning process, STTT, 9, 3-4, 255-267 (2007) |
| [44] | Barnat, J.; Brim, L.; Simecek, P.; Weber, M., Revisiting resistance speeds up i/o efficient LTL model checking, (TACAS. TACAS, LNCS, vol. 4963 (2008), Springer), 48-62 · Zbl 1134.68397 |
| [45] | Brim, L.; Cerná, I.; Moravec, P.; Simsa, J., Accepting predecessors are better than back edges in distributed ltl model-checking, (FMCAD. FMCAD, LNCS, vol. 3312 (2004), Springer), 352-366 · Zbl 1117.68422 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
