Abstract
Here we look in depth at the state explosion problem and the related parameterised verification problem: how to prove a property of a general class of processes or networks. We look at induction and data independence separately, and combine them into data independent induction, which can handle many networks that neither parent method can. These include networks based on one of the routing examples from Chap. 4, which are proved correct in general. We study the topic of buffer tolerance: when can we prove a property of a system with buffered channels by studying the corresponding unbuffered network, typically with a much smaller state space. This is closely related to the data flow model of concurrency. Finally, we study how Counter-Example Guided Abstraction Refinement (CEGAR) can be integrated naturally into FDR.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
In fact, as discussed on p. 362, CSP refinement over any of the models we have seen also has a high complexity: PSPACE-complete in the number of states of the specification process. In this case, and possibly also some of the cases alluded to above, the worst case behaviour is only rarely seen. However, in the literature on infinite-state decision problems the complexity classes involved are often very much higher than PSPACE-complete. See [101], for example.
- 2.
Where there is such a threshold N the answer for sufficiently large finite T also applies to all infinite T.
- 3.
In the case where there are constant symbols and the allowance discussed above has been made for these in the threshold (so this is no longer 1), you may test for equality and inequality with these values.
- 4.
It is legitimate to use complex prefixes such as c$x$y?z, but for technical reasons (see [80]) you may not mix (either here or anywhere else the nondeterministic selection construct is used in the study of data-independence) nondeterministic selections over T with inputs over types other than T.
- 5.
It is, at least in this case, straightforward to justify the simultaneous use of data independence theorems on two types at once. Since the type of messages is NoEqT data independent we know, for the refinements we are checking, that establishing them for a message type of size 2 is equivalent to establishing them for a large type with an arbitrary type of Names. It follows that we can fix the message type as {0,1}, say, before we start inducting over Names.
- 6.
In purely formal terms, we replace the test S(x) for satisfaction of the predicate symbol S by S(x)∨(x=c) where c is a constant symbol representing the name of the added node.
- 7.
In our implementation below we will rename each action of the form swap.Up.x.y in the lower process to swap.Up.y.x: this is easier to set out than separately linking all these pairs of channels. This “swapping of swap” is necessary so that the swapping of messages actually happens on a synchronisation.
- 8.
In fact this is equivalent to saying it is weakly buffer tolerant with respect to being a buffer since, you cannot make a non-buffer into a buffer by adding further buffering (see BL2 and BL3 in TPC).
- 9.
In other words, we can check one process with many added buffers, or many processes each of which has a single added buffer.
References
Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs. In: Proceedings of SAS (1997)
Boigelot, B., Wolper, P.: Verifying systems with infinite but regular state spaces. In: Proceedings of CAV (1998)
Buschmann, T.: Efficient checking for parallel attacks in Casper. Oxford University M.Sc. Dissertation (2006)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV 00. LNCS, vol. 1855. Springer, Berlin (2000)
Creese, S.J.: Data independent induction: CSP model checking of arbitrary sized networks. Oxford University D.Phil. Thesis (2001)
Creese, S.J., Roscoe, A.W.: TTP: a case study in combining induction and data independence. Oxford University Computing Laboratory Technical Report (1998)
Creese, S.J., Roscoe, A.W.: Verifying an infinite family of inductions simultaneously using data independence and FDR. In: FORTE/PSTV’99, 5–8 October 1999
Creese, S.J., Roscoe, A.W.: Data independent induction over structured networks. In: Proceedings of PDPTA2000
Godefroid, P., Long, D.E.: Symbolic protocol verification with queue BDDs. Form. Methods Syst. Des. 14(3), 257–271 (1999)
Josephs, M.B.: Receptive process theory. Acta Inform. 29, 17–31 (1992)
Kahn, G., MacQueen, D.B.: Coroutines and networks of parallel processes. In: Information Processing. North-Holland, Amsterdam (1977)
Kleiner, E.: A web services security study using Casper and FDR, 2008. Oxford University D.Phil. Thesis (2008)
Lazić, R.S.: A semantic study of data-independence with applications to the mechanical verification of concurrent systems. Oxford University D.Phil. Thesis (1997)
Lazić, R.S., Newcomb, T.C., Roscoe, A.W.: On model checking data-independent systems with arrays without reset. Theory Pract. Log. Program. 4, 5–6 (2004)
Lazić, R.S., Newcomb, T., Roscoe, A.W.: Polymorphic systems with arrays, 2-counter machines and multiset rewriting. In: Proceedings of INFINITY (2004)
Lazić, R.S., Newcomb, T., Roscoe, A.W., Worrell, J.B.: Nets with tokens which carry data. Fundam. Inform. 20, 251–274 (2008)
Ouaknine, J., Worrell, J.B.: On the decidability of metric temporal logic. In: LICS (2005)
Roscoe, A.W.: Finitary refinement checks for infinitary specifications. In: Proceedings of CPA (2004)
Roscoe, A.W.: The pursuit of buffer tolerance (2005). web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/106.pdf
Roscoe, A.W., Broadfoot, P.J.: Proving security protocols with model checkers by data independence techniques. J. Comput. Secur. 7, 147–190 (1999)
Roscoe, A.W., Lazić, R.S.: What can you decide about resetable arrays. In: Proc. VCL2001
Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: Proceedings of the 13th ACM POPL (1986)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer-Verlag London Limited
About this chapter
Cite this chapter
Roscoe, A.W. (2010). State Explosion and Parameterised Verification. In: Understanding Concurrent Systems. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-1-84882-258-0_17
Download citation
DOI: https://doi.org/10.1007/978-1-84882-258-0_17
Publisher Name: Springer, London
Print ISBN: 978-1-84882-257-3
Online ISBN: 978-1-84882-258-0
eBook Packages: Computer ScienceComputer Science (R0)