=Paper=
{{Paper
|id=None
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-1160/frontmatter.pdf
|volume=Vol-1160
}}
==None==
https://ceur-ws.org/Vol-1160/frontmatter.pdf
Editors: Daniel Moldt and
Heiko Rölke
Proceedings of the
International Workshop on
P etri
N ets and
S oftware
E ngineering
PNSE’14
University of Hamburg
Department of Informatics
These proceedings are published online by the editors as Volume 1160 at
CEUR Workshop Proceedings
ISSN 1613-0073
http://ceur-ws.org/Vol-1160
Copyright c 2014 for the individual papers is held by the papers’ authors. Copying
is permitted only for private and academic purposes. This volume is published and
copyrighted by its editors.
Preface
These are the proceedings of the International Workshop on Petri Nets and
Software Engineering (PNSE’14) in Tunis, Tunisia, June 23–24, 2014. It is
a co-located event of Petri Nets 2014, the 35th international conference on
Applications and Theory of Petri Nets and Concurrency and ACSD 2014,
the 14th 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/pnse14/
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, will be presented as well as their application and tools supporting
the disciplines mentioned above.
The program committee consists of:
Kamel Barkaoui (Conservatoire National des Arts et Métiers, France)
Robin Bergenthum (University of Hagen, Germany)
Didier Buchs (University of Geneva, Switzerland)
Lawrence Cabac (University of Hamburg, Germany)
Christine Choppy (Paris-North University (LIPN), France)
Piotr Chrzastowski-Wachtel (University of Warsaw, Poland)
José-Manuel Colom (University of Zaragoza, Spain)
Raymond Devillers (Université Libre de Bruxelles, Belgium)
Jorge C.A. de Figueiredo (Federal University of Campina Grande, Brazil)
Luís Gomes (Universidade Nova de Lisboa, Portugal)
Nicolas Guelfi (University of Luxembourg)
Stefan Haar (ENS Cachan, France)
Serge Haddad (ENS Cachan, France)
Xudong He (Florida International University, USA)
Thomas Hildebrandt (IT University of Copenhagen, Denmark)
Lom-Messan Hillah (University P. & M. Curie, LIP 6, France)
Kunihiko Hiraishi (Japan Advanced Institute of Science and Technology, Japan)
Vladimír Janoušek (Brno University of Technology, Czech Republic)
Peter Kemper (College of William and Mary, USA)
Astrid Kiehn (IIIT Delhi, India)
Ekkart Kindler (Technical University of Denmark, Denmark)
4 PNSE’14 – Petri Nets and Software Engineering
Hanna Klaudel (Université d’Evry-Val d’Essonne, France)
Radek Kočí (Brno University of Technology, Czech Republic)
Lars Kristensen (Bergen University College, Norway)
Michael Köhler-Bußmeier (University of Applied Science Hamburg, Germany)
Niels Lohmann (University of Rostock, Germany)
Robert Lorenz (University of Augsburg, Germany)
Daniel Moldt (University of Hamburg, Germany) (Chair)
Berndt Müller (University of South Wales, United Kingdom)
Chun Ouyang (Queensland University of Technology, Australia)
Wojciech Penczek (ICS PAS and Siedlce UPH, Poland)
Laure Petrucci (University Paris 13, France)
Lucia Pomello (Università degli Studi di Milano-Bicocca, Italy)
Heiko Rölke (DIPF, Germany) (Chair)
Christophe Sibertin-Blanc (Université Toulouse 1, France)
Mark-Oliver Stehr (SRI International)
Harald Störrle (Technical University of Denmark, Denmark)
Eric Verbeek (Eindhoven University of Technology, Netherlands)
Jan Martijn van der Werf (Utrecht University, Netherlands)
Manuel Wimmer (Vienna University of Technology, Austria)
Karsten Wolf (University of Rostock, Germany)
There is one invited talk by Lars Kristensen from Bergen University Col-
lege, Norway. We received more than 28 high-quality contributions. For
each paper three to four reviews were made. The program committee has
accepted five of them for full presentation. Furthermore the committee ac-
cepted 13 papers as short presentations and one short paper. Several more
contributions were submitted and accepted as posters.
The international program committee was supported by the valued work of
following sub reviewers: Sofiane Bendoukha, Maximilien Colange, Tadeusz
Czachorski, Markus Huber, Yasir Khan, Görkem Kılınç, Luca Manzoni, Artur
Niewiadomski, and Józef Winkowski. Their work is highly appreciated.
Furthermore, we would like to thank our colleagues in the local organization
in Tunis, Tunisia, 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.
Thank you,
Daniel Moldt and Heiko Rölke Hamburg, June 2014
Contents
PNSE’14 Proceedings
Contents
Part I PNSE’14: Invited Talk
An Approach for the Engineering of Protocol Software from
Coloured Petri Net Models:
A Case Study of the IETF WebSocket Protocol
Lars Michael Kristensen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
Part II PNSE’14: Long Presentations
Verification of Logs - Revealing Faulty Processes of a Medical
Laboratory
Robin Bergenthum and Joachim Schick . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
On-The-Fly Model Checking of Times Properties on Time
Petri Nets
Kais Klai . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
SMT-based Abstract Temporal Planning
Artur Niewiadomski and Wojciech Penczek . . . . . . . . . . . . . . . . . . . . . . . . . . 55
Kleene Theorems for Labelled Free Choice Nets
Ramchandra Phawade and Kamal Lodaya . . . . . . . . . . . . . . . . . . . . . . . . . . 75
Using Symbolic Techniques and Algebraic Petri Nets to
Model Check Security Protocols for Ad-Hoc Networks
Mihai Lica Pura and Didier Buchs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
Part III PNSE’14: Short Presentations
Morphisms on Marked Graphs
Luca Bernardinello, Lucia Pomello and Stefano Scaccabarozzi . . . . . . . . . 113
A Petri Net Approach for Reusing and Adapting Components
with Atomic and non-atomic Synchronisation
Djaouida Dahmani, Mohand Cherif Boukala and Hassan Mountassir . . . 129
Observable Liveness
Jörg Desel and Görkem Kılınç . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143
Real-Time Property Specific Reduction for Time Petri Net
Ning Ge and Marc Pantel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
Visual Language Plans - Formalization of a Pedagogical
Learnflow Modeling Language
Kerstin Irgang and Thomas Irgang . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
Slicing High-level Petri Nets
Yasir Imtiaz Khan and Nicolas Guelfi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201
Performance Analysis of M/G/1 Retrial Queue with Finite
Source Population Using Markov Regenerative Stochastic
Petri Nets
Ikhlef Lyes, Lekadir Ouiza and Djamil Aïssani . . . . . . . . . . . . . . . . . . . . . . . 221
Petri Nets Based Approach for Modular Verification of
SysML Requirements on Activity Diagrams
Messaoud Rahim, Malika Boukala-Ioualalen and Ahmed Hammad . . . . . . 233
Compatibility Analysis of Time Open Workflow Nets
Zohra Sbaï, Kamel Barkaoui and Hanifa Boucheneb . . . . . . . . . . . . . . . . . . 249
Petra: A Tool for Analysing a Process Family
Dennis Schunselaar, Eric Verbeek, Wil van der Aalst and
Hajo A. Reijers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 269
An Evaluation of Automated Code Generation with the
PetriCode Approach
Kent Inge Fagerland Simonsen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 289
Computing Minimal Siphons in Petri Net Models of Resource
Allocation Systems: An Evolutionary Approach
Fernando Tricas, José Manuel Colom and Juan Julián Merelo . . . . . . . . . 307
Part IV PNSE’14: Short Papers
Persistency and Nonviolence Decision Problems in P/T-Nets
with Step Semantics
Kamila Barylska . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 325
Part V PNSE’14: Poster Abstracts
Construction of Data Streams Applications from Functional,
Non-Functional and Resource Requirements for Electric
Vehicle Aggregators. The COSMOS Vision
José Ángel Bañares, Rafael Tolosana-Calasanz, Fernando Tricas, Unai
Arronategui, Javier Celaya and José Manuel Colom . . . . . . . . . . . . . . . . . . 333
Modular Modeling of SMIL Documents with Complex
Termination Events
Djaouida Dahmani, Samia Mazouz and Malika Boukala . . . . . . . . . . . . . . . 335
D&A4WSC as a Design and Analysis Framework of Web
Services Composition
Rawand Guerfel and Zohra Sbaï . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 337
Constructing Petri Net Transducers with PNT"ooL
Markus Huber and Robert Lorenz . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 339
SLAPN : A Tool for Slicing Algebraic Petri Nets
Yasir Imtiaz Khan and Nicolas Guelfi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 343
Generating CA-Plans from Multisets of Services
Łukasz Mikulski, Artur Niewiadomski, Marcin Piątkowski and
Sebastian Smyczyński . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 347
LoLA as Abstract Planning Engine of PlanICS
Artur Niewiadomski and Karsten Wolf . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 349
PlanICS 2.0 - A Tool for Composing Services
Artur Niewiadomski and Wojciech Penczek . . . . . . . . . . . . . . . . . . . . . . . . . . 351
Petri Net Simulation as a Service
Petr Polasek, Vladimir Janousek and Milan Ceska . . . . . . . . . . . . . . . . . . . 353