=Paper=
{{Paper
|id=None
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-851/frontmatter.pdf
|volume=Vol-851
}}
==None==
https://ceur-ws.org/Vol-851/frontmatter.pdf
Editors: Lawrence Cabac,
Michael Duvigneau and
Daniel Moldt
Proceedings of the
International Workshop on
P etri
N ets and
S oftware
E ngineering
PNSE’12
University of Hamburg
Department of Informatics
These proceedings are published online by the editors as Volume 851 at
CEUR Workshop Proceedings
ISSN 1613-0073
http://ceur-ws.org/Vol-851
A printed version is published as FB-Mitteilung FBI-HH-M-346/12 by
Fachbereich Informatik
Universität Hamburg
Vogt-Kölln-Straße 30
22527 Hamburg, Germany
Copyright for the individual papers is held by the papers’ authors. Copying is per-
mitted only for private and academic purposes. This volume is published and copy-
righted by its editors.
Preface
These are the proceedings of the International Workshop on Petri Nets and
Software Engineering (PNSE’12) in Hamburg, Germany, June 25–26, 2012.
It is a co-located event of Petri Nets 2012, the 33rd international conference
on Applications and Theory of Petri Nets and Concurrency, and ACSD 2012,
the 12th International Conference on Application of Concurrency to System
Design.
More information about the workshop can be found at
http://www.informatik.uni-hamburg.de/TGI/events/pnse12/
For the successful realisation of complex systems of interacting and reactive
software and hardware components the use of a precise language at different
stages of the development process is of crucial importance. Petri nets are be-
coming increasingly popular in this area, as they provide a uniform language
supporting the tasks of modelling, validation, and verification. Their popular-
ity is due to the fact that Petri nets capture fundamental aspects of causality,
concurrency and choice in a natural and mathematically precise way without
compromising readability.
The use of Petri nets (P/T-nets, coloured Petri nets and extensions) in
the formal process of software engineering, covering modelling, validation,
and verification, is presented as well as their application and tools supporting
the disciplines mentioned above.
The program committee consists of:
Kamel Barkaoui (France)
Didier Buchs (Switzerland)
Lawrence Cabac (Germany) (Chair)
Piotr Chrzastowski-Wachtel (Poland)
Gianfranco Ciardo (USA)
José-Manuel Colom (Spain)
Jörg Desel (Germany)
Raymond Devillers (Belgium)
Michael Duvigneau (Germany) (Chair)
Jorge C.A. de Figueiredo (Brasilia)
Luís Gomes (Portugal)
Stefan Haar (France)
Xudong He (USA)
Thomas Hildebrandt (Danmark)
Kunihiko Hiraishi (Japan)
Vladimir Janousek (Czech republic)
Peter Kemper (USA)
Hanna Klaudel (France)
4 PNSE’12 – Petri Nets and Software Engineering
Radek Koci (Czech republic)
Fabrice Kordon (France)
Lars Kristensen (Norway)
Johan Lilius (Finland)
Niels Lohmann (Germany)
Daniel Moldt (Germany) (Chair)
Berndt Müller (Great Britain)
Chun Ouyang (Australia)
Wojciech Penczek (Poland)
Laure Petrucci (France)
Lucia Pomello (Italy)
Heiko Rölke (Germany)
Catherine Tessier (France)
H.M.W. (Eric) Verbeek (Netherlands)
We received 27 high-quality contributions. The program committee has ac-
cepted eight of them for full presentation. Furthermore the committee ac-
cepted four papers as short presentations. Eight more contributions were ac-
cepted as posters.
The international program committee was supported by the valued work
of Paulo Barbosa, Robin Bergenthum, Luca Bernardinello, Jean-Yves Di-
dier, Bachir Djafri, Carlo Ferigato, Agata Janowska, Alban Linard, Edmundo
Lopez, Romain Soulat, and Maciej Szreter as additional reviewers. Their work
is highly appreciated.
Furthermore, we would like to thank our colleagues in the local organization
team here at the University of Hamburg, Germany, for their support.
Without the enormous efforts of authors, reviewers, PC members and the or-
ganizational team this workshop wouldn’t provide such an interesting booklet.
Thanks!
Lawrence Cabac, Michael Duvigneau, Daniel Moldt
Hamburg, June 2012
Contents
Part I Invited Talks
What Should we Teach About Petri Nets?
Wolfgang Reisig . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
Part II Long Presentations
Using Integer Time Steps for Checking Branching Time
Properties of Time Petri Nets
Agata Janowska, Wojciech Penczek, Agata Półrola and Andrzej Zbrzezny 15
Grade/CPN: Semi-automatic Support for Teaching Petri
Nets by Checking Many Petri Nets Against One Specification
Michael Westergaard, Dirk Fahland and Christian Stahl . . . . . . . . . . . . . . . 32
When Can We Trust a Third Party? - A Soundness
Perspective
Kees van Hee, Natalia Sidorova and Jan Martijn van der Werf . . . . . . . . 47
Modeling and Analyzing Wireless Sensor Networks with
VeriSensor
Yann Ben Maissa, Fabrice Kordon, Salma Mouline and Yann
Thierry-Mieg . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
SMT-based parameter synthesis for L/U automata
Michał Knapik and Wojciech Penczek . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
Model-Driven Middleware Support for Team-Oriented
Process Management
Matthias Wester-Ebbinghaus and Michael Köhler-Bußmeier . . . . . . . . . . . 93
6 Contents
From Code to Coloured Petri Nets: Modelling Guidelines
Anna Dedova and Laure Petrucci . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
Hierarchy of persistency with respect to the length of action’s
disability
Kamila Agata Barylska and Edward Ochmański . . . . . . . . . . . . . . . . . . . . . . 125
Part III Short Presentations
Local state refinement on Elementary Net Systems: an
approach based on morphisms
Luca Bernardinello, Elisabetta Mangioni and Lucia Pomello . . . . . . . . . . . 141
Context Petri Nets: Enabling Consistent Composition of
Context-dependent Behavior
Nicolás Cardozo, Jorge Vallejos, Sebastián González, Kim Mens and
Theo D’Hondt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156
MuPSi - a multitouch Petri net simulator for transition steps
Thomas Irgang, Andreas Harrer and Robin Bergenthum . . . . . . . . . . . . . . . 171
PetriPad – A Collaborative Petri Net Editor
Julian Burkhart and Michael Haustermann . . . . . . . . . . . . . . . . . . . . . . . . . . 182
Part IV Poster Abstracts
Agentworkflows for Flexible Workflow Execution
Thomas Wagner . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199
Cloud Transition: Integrating Cloud Calls into Workflow
Petri Nets
Sofiane Bendoukha and Thomas Wagner . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215
A Concurrent Simulator for Petri Nets Based on the
Paradigm of Actors of Hewitt
Luca Bernardinello and Francesco Adalberto Bianchi . . . . . . . . . . . . . . . . . 217
A Petri Net Approach to Synthesize Intelligible State
Machine Models from Choreography
Toshiyuki Miyamoto and Yasuwo Hasegawa . . . . . . . . . . . . . . . . . . . . . . . . . 222
SYNOPS - Generation of Partial Languages and Synthesis of
Petri Nets
Robert Lorenz, Markus Huber, Christoph Etzel and Dan Zecha . . . . . . . . . 237
Contents 7
Modeling and Simulation-Based Design Using Object-
Oriented Petri Nets: A Case Study
Radek Kočí and Vladimír Janoušek . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 253
Porting the Renew Petri Net Simulator to the Operating
System Android
Dominic Dibbern . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267
SonarEditor: A Tool for Multi-Agent-Organizations Modelling
Jan Bolte . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 269