Affiliations: Department of Computing Science, University of
Oldenburg. D-26129 Oldenburg, Germany. E-mail:
{Roland.Meyer,Tim.Strazny}@informatik.uni-oldenburg.de | School of Computing Science, Newcastle University,
Newcastle upon Tyne, NE1 7RU, U.K. E-mail: [email protected]
Abstract: 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.
Keywords: finite control processes, safe processes, π-Calculus, mobile systems, model checking, Petri net unfoldings
