Local Verification Using a Distributed State Space

• Autorzy: Abid C. A. , Zouari B.
• Języki publikacji: EN

Abstrakty

EN

This paper deals with the modular analysis of distributed concurrent systems modelled by Petri nets. The main analysis techniques of such systems suffer from the well-known problem of the combinatory explosion of state space. In order to cope with this problem, we use a modular representation of the state space instead of the ordinary one. The modular representation, namely modular state space, is much smaller than the ordinary state space. We propose to distribute the modular state space on every machine associated with one module. We enhance the modularity of the verification of some local properties of any module by limiting it to the exploration of local and some global information. Once the construction of the distributed state space is performed, there is no communication between modules during the verification.

Słowa kluczowe

EN

distributed systems; modular verification; Petri nets; state space explosion

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 125, nr 1
• Strony: 1--20
• Opis fizyczny: Bibliogr. 21 poz., wykr.

Twórcy

autor

Abid C. A.

• LIP2 Laboratory, University of Tunis - El Manar 2092, Tunis, Tunisia

autor

Zouari B.

• LIP2 Laboratory, University of Tunis - El Manar 2092, Tunis, Tunisia

Bibliografia

• [1] Abid, C. A., Zouari, B.: A distributed verification approach for modular Petri nets, SCSC: Proceedings of the 2007 summer computer simulation conference, Society for Computer Simulation International, San Diego, CA, USA, 2007, ISBN 1-56555-316-0.
• [2] Abid, C. A., Zouari, B.: Decentralized Active Controller, Proceedings of 7th International Conference on Informatics in Control, Automation and Robotics (ICINCO 2010), Vol 2, Madeira, Portugal, June 2010.
• [3] Baldwin, C., Clark, K.: Managing modularity, Harvard Business Review, 75(5), 1997, 84-93.
• [4] Barnat, J., Cerna, I.: Distributed breadth-first search LTL model checking, Formal Methods in System Design, 29(2), 2006, 117-134.
• [5] Boukala, C., Petrucci, L.: Towards Distributed Verification of Petri Nets properties, Proc. 1st International Workshop on Verification and Evaluation of Computer and Communication Systems (VECOS’07), Algiers, Algeria, eWiC, British Computer Society, May 2007.
• [6] Christensen, S., Petrucci, L.: Modular Analysis of Petri Nets, Comput. J., 43(3), 2000, 224-242.
• [7] Ciardo, G.: Distributed and Structured Analysis Approaches to Study Large and Complex Systems, Lectures on Formal Methods and Performance Analysis, LNCS 2090, Springer-Verlag, 2001.
• [8] Grumberg, O., Heyman, T., Schuster, A.: A work-efficient distributed algorithm for reachability analysis, Form. Methods Syst. Des., 29(2), 2006, 157-175, ISSN 0925-9856.
• [9] Heyman, T., Grumberg, O., Schuster, A.: A work-efficient distributed algorithm for reachability analysis, CAV: International Conference on Computer Aided Verification, 2003.
• [10] Kindler, E., Petrucci, L.: Towards a standard for modular Petri nets: A formalisation, Applications and Theory of Petri Nets, 2009, 43-62.
• [11] Klai, K., Petrucci, L., Reniers, M.: An Incremental and Modular Technique for Checking LTL/X Properties of Petri Nets, FORTE 07: Proceedings of the 27th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems, Springer-Verlag, Berlin, Heidelberg, 2007, ISBN 978-3-540-73195-5.
• [12] Kristensen, L. M., Petrucci, L.: An Approach to Distributed State Space Exploration for Coloured Petri Nets, ICATPN, 2004.
• [13] Lakos, C., Petrucci, L.: Modular Analysis of Systems Composed of Semiautonomous Subsystems, ACSD, 2004.
• [14] Lakos, C., Petrucci, L.: Distributed and modular state space exploration for timed petri nets, Workshop on Practical Use of Coloured Petri Nets, Aarhus, Denmark, October 2005.
• [15] Li, H. C., Fisler, K., Krishnamurthi, S.: The Influence of Software Module Systems on Modular Verification, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, Springer-Verlag, London, UK, 2002, ISBN 3-540-43477-1.
• [16] Makela, M.: Model Checking Safety Properties in Modular High-Level Nets, 24th International Conference on the Application and Theory of Petri Nets (ICATPN 2003). Volume 2679 ofLNCS., Springer, 2003.
• [17] McMillan, K. L., Qadeer, S., Saxe, J. B.: Induction in Compositional Model Checking, CAV, 2000.
• [18] Righini, G.: Modular Petri Nets for simulation of flexible production systems, International Journal of Production Research, 31(10), 1993, 2463-2477.
• [19] Valmari, A.: Compositional State Space Generation, Applications and Theory of Petri Nets, 1991.
• [20] Valmari, A., Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm, PSTV, 1991.
• [21] Xiao-wei, H., Wei-ming, L.: A Modular Petri Net For The Asynchronous Communications, Journal of System Simulation, 2007.