Abstract
In this paper we propose a technique for verification of mobile systems. We translate finite control processes, which are a well-known subset of π-Calculus, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe processes, which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime.
This is a preview of subscription content, log in via an institution to check access.
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
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Dam, M.: Model checking mobile processes. Information and Computation 129(1), 35–51 (1996)
Esparza, J., Heljanko, K.: Implementing LTL model checking with net unfoldings. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 37–56. Springer, Heidelberg (2001)
Esparza, J., Römer, S., Vogler, W.: An Improvement of McMillan’s Unfolding Algorithm. Formal Methods in System Design 20(3), 285–310 (2002)
Esparza, J.: Decidability and complexity of Petri net problems — an introduction. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998)
Ferrari, G.-L., Gnesi, S., Montanari, U., Pistore, M.: A model-checking verification environment for mobile processes. ACM Transactions on Software Engineering and Methodology 12(4), 440–473 (2003)
Khomenko, V.: Model Checking Based on Prefixes of Petri Net Unfoldings. PhD thesis, School of Computing Science, Newcastle University (2003)
Khomenko, V., Koutny, M., Niaouris, A.: Applying Petri net unfoldings for verification of mobile systems. In: Proc. Workshop on Modelling of Objects, Components and Agents (MOCA 2006), Bericht FBI-HH-B-267/06, pp. 161–178. University of Hamburg (2006)
Khomenko, V., Koutny, M., Yakovlev, A.: Detecting state coding conflicts in STG unfoldings using SAT. Fundamenta Informaticae 62(2), 1–21 (2004)
McMillan, K.: Using unfoldings to avoid state explosion problem in the verification of asynchronous circuits. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 164–174. Springer, Heidelberg (1993)
Meyer, R.: A theory of structural stationarity in the π-Calculus (under revision) (2007)
Milner, R.: Communicating and Mobile Systems: the π−Calculus. Cambridge University Press, Cambridge (1999)
Meyer, R., Khomenko, V., Strazny, T.: A practical approach to verification of mobile systems using net unfoldings. Technical Report CS-TR-1064, School of Computing Science, Newcastle University (2008), URL: http://www.cs.ncl.ac.uk/research/pubs/trs/abstract.php?number=1064
Orava, F., Parrow, J.: An algebraic verification of a mobile network. Formal Aspects of Computing 4(6), 497–543 (1992)
Pistore, M.: History Dependent Automata. PhD thesis, Dipartimento di Informatica, Università di Pisa (1999)
Sangiorgi, D., Walker, D.: The π-Calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Valmari, A.: Lectures on Petri Nets I: Basic Models. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Victor, B., Moller, F.: The mobility workbench: A tool for the π−Calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 428–440. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meyer, R., Khomenko, V., Strazny, T. (2008). A Practical Approach to Verification of Mobile Systems Using Net Unfoldings. In: van Hee, K.M., Valk, R. (eds) Applications and Theory of Petri Nets. PETRI NETS 2008. Lecture Notes in Computer Science, vol 5062. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68746-7_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-68746-7_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68745-0
Online ISBN: 978-3-540-68746-7
eBook Packages: Computer ScienceComputer Science (R0)