A Practical Approach to Verification of Mobile Systems Using Net Unfoldings

• Autorzy: Meyer R. , Khomenko V. , Strazny T.
• Języki publikacji: EN

Abstrakty

EN

We propose a technique for verification of mobile systems. We translate finite control processes, a well-known subset of π-Calculus, into Petri nets, which are subsequently used formodel 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, 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. We also demonstrate the applicability of our method on a realistic model of an automated manufacturing system.

Słowa kluczowe

EN

finite control processes; safe processes; pi-calculus; mobile systems; model checking; Petri net unfoldings

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 94, nr 3/4
• Strony: 4439--471
• Opis fizyczny: Bibliogr. 33 poz., tab., wykr.

Twórcy

autor

Meyer R.

autor

Khomenko V.

autor

Strazny T.

• School of Computing Science, Newcastle University, Newcastle upon Tyne, NE1 7RU, U.K.,

Bibliografia

• [1] Amadio, R. M., Meyssonnier, C.: On Decidability of the Control Reachability Problem in the Asynchronous _-Calculus., Nordic Journal of Computing, 9(1), 2002, 70-101.
• [2] Braatz, A., Ritter, A.: Referenzfallstudie Produktionstechnik, Technical report, IFF University Stuttgart and Fraunhofer IPA Stuttgart, 2001, Version 1.3: http://tfs.cs.tu-berlin.de/projekte/indspec/SPP/ RefPAv13.ps, Version 2.0: http://tfs.cs.tu-berlin.de/projekte/indspec/SPP/RefPAv2.ps.
• [3] Busi, N.: Analysis issues in Petri nets with inhibitor arcs, Theoretical Computer Science, 275(1-2), 2002, 127-177.
• [4] Busi, N., Gorrieri, R.: A Petri Net Semantics for _-Calculus, Proc. CONCUR'95, 962, Springer, 1995.
• [5] Busi, N., Gorrieri, R.: Distributed semantics for the _-calculus based on Petri nets with inhibitor arcs, Journal of Logic and Algebraic Programming, 78(1), 2009, 138-162.
• [6] Clarke, E., Grumberg, O., Peled, D.: Model Checking, MIT Press, 1999.
• [7] Dam, M.: Model Checking Mobile Processes, Information and Computation, 129(1), 1996, 35-51.
• [8] Devillers, R., Klaudel, H., Koutny, M.: A Petri Net Semantics of the Finite _-Calculus Terms, Fundamenta Informaticae, 70(3), 2006, 203-226.
• [9] Devillers, R., Klaudel, H., Koutny, M.: A compositional Petri net translation of general _-calculus terms, Formal Aspects of Computing, 20(4-5), 2008, 429-450.
• [10] Engelfriet, J.: A Multiset Semantics for the _-Calculus with Replication, Theoretical Computer Science, 153(1-2), 1996, 65-94.
• [11] Esparza, J.: Decidability and Complexity of Petri Net Problems - an Introduction, in: Lectures on Petri Nets I: Basic Models (W. Reisig, G. Rozenberg, Eds.), vol. 1491 of LNCS, Springer, 1998, 374-428.
• [12] Esparza, J., Rőmer, S., Vogler, W.: An Improvement of McMillan's Unfolding Algorithm, Formal Methods in System Design, 20(3), 2002, 285-310.
• [13] 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), 2003, 440-473.
• [14] Flake, S., Müller, W., Pape, U., Ruf, J.: Analyzing Timing Constraints in Flexible Manufacturing Systems, Proc. IAM'01, 2001.
• [15] Gringel, P.: Modellierung und Verifikation eines holonischen Transportsystems mit dem Pi-Kalkül, Bachelor's thesis, Department of Computing Science, University of Oldenburg, 2007.
• [16] Khomenko, V.: Model Checking Based on Prefixes of Petri Net Unfoldings, Ph.D. Thesis, School of Computing Science, Newcastle University, 2003.
• [17] Khomenko, V., Koutny,M., Niaouris, A.: Applying Petri Net Unfoldings for Verification ofMobile Systems, Proc. MOCA'06, Bericht FBI-HH-B-267/06, University of Hamburg, 2006.
• [18] Khomenko, V., Koutny, M., Yakovlev, A.: Detecting State Coding Conflicts in STG Unfoldings Using SAT, Fundamenta Informaticae, 62(2), 2004, 1-21.
• [19] Mayr, E., Meyer, A.: The Complexity of the Finite Containment Problem for Petri Nets, Journal of the ACM, 28(3), 1981, 561-576.
• [20] McMillan, K.: Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits, Proc. CAV'92, 663, Springer, 1992.
• [21] Meyer, R.: Structural Stationarity in the _-Calculus , Ph.D. Thesis, Department of Computing Science, University of Oldenburg, 2008.
• [22] Meyer, R.: A theory of structural stationarity in the _-Calculus, Acta Informatica, 46(2), 2009, 87-137.
• [23] Milner, R.: Communicating and Mobile Systems: the _-Calculus , Cambridge University Press, 1999.
• [24] Mőller, M., Olderog, E.-R., Rasch, H., Wehrheim, H.: Linking CSP-OZ with UML and Java: A Case Study, Proc. IFM'04, 2999, Springer, 2004.
• [25] Montanari, U., Pistore, M.: Checking Bisimilarity for Finitary _-Calculus, Proc. CONCUR'95, 962, Springer, 1995.
• [26] Montanari, U., Pistore, M.: History Dependent Automata, Technical report, Instituto Trentino di Cultura, 2001.
• [27] Orava, F., Parrow, J.: An Algebraic Verification of a Mobile Network, Formal Aspects of Computing, 4(6), 1992, 497-543.
• [28] Pistore, M.: History Dependent Automata, Ph.D. Thesis, Dipartimento di Informatica, Università di Pisa, 1999.
• [29] Ruf, J., Weiss, J., Kropf, T., Rosenstiel, W.: Modeling and Formal Verification of Production Automation Systems., Proc. INT'04, 3147, Springer, 2004.
• [30] Sangiorgi, D., Walker, D.: The π-Calculus: a Theory of Mobile Processes, Cambridge University Press, 2001.
• [31] Valmari, A.: The State Explosion Problem, in: Lectures on Petri Nets I: Basic Models (W. Reisig, G. Rozenberg, Eds.), vol. 1491 of LNCS, Springer, 1998, 429-528.
• [32] Victor, B., Moller, F.: The Mobility Workbench: A Tool for the π-Calculus, Proc. CAV'94, 818, Springer, 1994.
• [33] Wehrheim, H.: Specification of an AutomaticManufacturing System: A case study in using integrated formal methods, Proc. FASE'00, 1783, Springer, 2000.