Abstract
Modelling and analysis of dynamic multi-threaded state systems often encounters obstacles when one wants to use automated verification methods, such as model checking. Our aim in this paper is to develop a technical device for coping with one such obstacle, namely that caused by dynamic process creation.
We first introduce a general class of coloured Petri nets—not tied to any particular syntax or approach—allowing one to capture systems with dynamic (and concurrent) process creation as well as capable of manipulating data. Following this, we introduce the central notion of our method which is a marking equivalence that can be efficiently computed and then used, for instance, to aggregate markings in a reachability graph. In some situations, such an aggregation may produce a finite representation of an infinite state system which still allows one to establish the relevant behavioural properties. We show feasibility of the method on an example and provide initial experimental results.
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 subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ball, T., Chaki, S., Rajamani, S.K.: Parameterized Verification of Multithreaded Software Libraries. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 158–173. Springer, Heidelberg (2001)
Best, E., et al.: M-Nets: An Algebra of High-Level Petri Nets, with an Application to the Semantics of Concurrent Programming Languages. Acta Informatica 35, 813–857 (1998)
Bosnacki, D., Dams, D., Holenderski, L.: Symmetric Spin. International Journal on Software Tools for Technology Transfer 4, 92–106 (2002)
Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: A Symbolic Reachability Graph for Coloured Petri Nets. Theoretical Computer Science 176, 39–65 (1997)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Corbett, J.C., et al.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proc. ICSE 2000, pp. 439–448. ACM, New York (2000)
Cordella, L.P., Foggia, P., Sansone, C., Vento, M.: A (Sub)Graph Isomorphism Algorithm for Matching Large Graphs. IEEE Transactions on Pattern Analysis and Machine Intelligence 26, 1367–1372 (2004)
Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. POPL 1977, pp. 238–252. ACM, New York (1977)
Delzanno, G.: Constraint-based Automatic Verification of Abstract Models of Multithreaded Programs. Journal of Theory and Practice of Logic Programming 7 (2007)
Evangelista, S.: High Level Petri Nets Analysis with Helena. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 455–464. Springer, Heidelberg (2005)
Flanagan, C., Freund, S.N., Qadeer, S., Seshia, S.A.: Modular Verification of Multithreaded Programs. Theoretical Computer Science 338, 153–183 (2005)
Hagberg, A., Schult, D., Swart, P.: NetworkX, High Productivity Software for Complex Networks, http://networkx.lanl.gov
Hendriks, M., et al.: Adding Symmetry Reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 46–59. Springer, Heidelberg (2004)
Khomenko, V.: Model Checking Based on Prefixes of Petri Net Unfoldings. PhD Thesis, School of Computing Science, University of Newcastle (2003)
Klaudel, H., Koutny, M., Pelz, E., Pommereau, F.: Towards Efficient Verification of Systems with Dynamic Process Creation. LACL Technical Report (2008), http://lacl.univ-paris12.fr
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems Specification. Springer, Heidelberg (1991)
McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Miller, A., Donaldson, A., Calder, M.: Symmetry in Temporal Logic Model Checking. ACM Comput. Surv. 38 (2006)
Pommereau, F.: Versatile Boxes, a Multi-Purpose Algebra of High-Level Petri Nets. In: DADS/SCSC 2007, SCS/ACM (2007)
Pommereau, F.: Quickly Prototyping Petri Net Tools with Snakes. In: Proc. PNTAP 2008, ACM Digital Library (2008)
Rabin, M.O.: Decidability of Second-order Theories and Automata on Infinite Trees. Transactions of the American Mathematical Society 141 (1969)
Rosa-Velardo, F., de Frutos-Escrig, D.: Name Creation vs. Replication in Petri Net Systems. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 402–422. Springer, Heidelberg (2007)
Stärk, R.F.: Formal Specification and Verification of the C# Thread Model. Theoretical Computer Science 343, 482–508 (2005)
Stoller, S.D.: Model-Checking Multi-threaded Distributed Java Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 224–244. Springer, Heidelberg (2000)
Thierry-Mieg, Y., Dutheillet, C., Mounier, I.: Automatic Symmetry Detection in Well-Formed Nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 82–101. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klaudel, H., Koutny, M., Pelz, E., Pommereau, F. (2008). Towards Efficient Verification of Systems with Dynamic Process Creation. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds) Theoretical Aspects of Computing - ICTAC 2008. ICTAC 2008. Lecture Notes in Computer Science, vol 5160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85762-4_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-85762-4_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85761-7
Online ISBN: 978-3-540-85762-4
eBook Packages: Computer ScienceComputer Science (R0)