Toggle Main Menu Toggle Search

Open Access padlockePrints

Applying Petri Net Unfoldings for Verification of Mobile Systems

Lookup NU author(s): Dr Victor Khomenko, Professor Maciej Koutny, Dr Apostolos Niaouris

Downloads

Full text for this publication is not currently held within this repository. Alternative links are provided below where available.


Abstract

Mobility is a central feature of many distributed systems of ever growing complexity. To make their formal analysis and verification feasible, process algebras - notably the pi-calculus - have been introduced and extensively studied. A well-established method of verifying the correctness of general distributed systems has been model-checking which is completely automatic and relatively fast compared to other alternatives, and so particularly attractive in industrial context. Mobile systems are highly concurrent causing state space explosion when applying model-checking techniques. To cope with this problem, techniques based on partial order semantics of concurrency seem to offer the desired level of efficiency. The aim of this paper is to investigate how one of such techniques - based of unfoldings of high-level Petri nets - could be used for verification of pi-calculus terms. Our starting point was an existing compositional translation from a finite fragment of the pi-calculus into a class of high-level Petri nets. We developed a prototype tool based on this theoretical translation and an existing efficient unfolder and verifier. In this paper, we describe initial experimental results in support of specific design choices. Crucially, developing the prototype was not a straightforward task since the theoretical translation does not produce nets which conform to the input format required by the verifier. The paper states how this mismatch has been overcome and draws conclusions for future uses of unfoldings technique in the model-checking of mobile systems.


Publication metadata

Author(s): Khomenko V, Koutny M, Niaouris A

Editor(s): Moldt, D.

Publication type: Conference Proceedings (inc. Abstract)

Publication status: Published

Conference Name: Fourth International Workshop on Modelling of Objects, Components and Agents (MOCA'06)

Year of Conference: 2006

Pages: 161-178

Publisher: Universit├Ąt Hamburg, Department Informatik

Notes: Proceedings published as Universit├Ąt Hamburg, Department Informatik, Bericht FBI-HH-B-272/06


Share