Tim Strazny

 

1 Publications (BibTeX Source)

@INPROCEEDINGS{MeyerKhomenkoStrazny2008Unfolding,
  AUTHOR = {R. Meyer and V. Khomenko and T. Strazny},
  TITLE = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
  BOOKTITLE = {Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008},
  SERIES = {LNCS},
  VOLUME = {5062},
  PUBLISHER = {Springer-Verlag},
  NOTE = {To appear},
  YEAR = {2008},
  KEYWORDS = {finite control processes, safe processes, $\pi$-Calculus, mobile
systems, model checking, Petri net unfoldings},
  ABSTRACT = {
In this paper we propose a technique for verification of mobile
systems.We translate finite control processes, which are a well-known
subset of $\pi$-Calculus, into Petri nets, which are subsequently used for
model 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 pro-
cesses, which are 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.}
}


@TECHREPORT{MeyerKhomenkoStrazny2008UnfoldingTR,
  AUTHOR = {R. Meyer and V. Khomenko and T. Strazny},
  TITLE = {A Practical Approach to Verification of Mobile Systems Using Net
Unfoldings},
  INSTITUTION = {School of Computing Science, Newcastle University},
  MONTH = {January},
  YEAR = {2008},
  NUMBER = {CS-TR: 1064},
  NOTE = {29 pages},
  KEYWORDS = {finite control processes, safe processes, $\pi$-Calculus, mobile
systems, model checking, Petri net unfoldings},
  ABSTRACT = {
In this paper we propose a technique for verification of mobile
systems.We translate finite control processes, which are a well-known
subset of $\pi$-Calculus, into Petri nets, which are subsequently used for
model 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 pro-
cesses, which are 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.
}
}


@INPROCEEDINGS{SS06,
  AUTHOR = {Tim Strazny and Christian Stehno},
  TITLE = {{E}in {S}imulator {f}\"{u}r {m}ehrfach {e}rweiterte
{h}\"{o}here {P}etrinetze},
  BOOKTITLE = {19. Symposium Simulationstechnik (ASIM 2006)},
  EDITOR = {Matthias Becker and Helena Szczerbicka},
  YEAR = {2006},
  MONTH = SEP,
  PAGES = {171--176},
  PUBLISHER = {SCS Publishing House e.V.},
}