=Paper=
{{Paper
|id=Vol-1591/frontmatter
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-1591/frontmatter.pdf
|volume=Vol-1591
}}
==None==
https://ceur-ws.org/Vol-1591/frontmatter.pdf
Proceedings
»PNSE’16«
International Workshop on
Petri Nets and Software Engineering
Satellite event of the
37th International Conference on
Application and Theory of Petri Nets
and Concurrency
16th International Conference on
Application of Concurrency to
System Design
Toruń, Poland, June, 2016
including papers of
»BioPPN’16«
International Workshop on
Biological Processes and Petri Nets
Editors: Lawrence Cabac,
Lars Michael Kristensen,
Heiko Rölke
Proceedings of the
International Workshop on
Petri
Nets and
Software
Engineering
PNSE’16
University of Hamburg
Department of Informatics
These proceedings are published online by the editors as Volume 1591 at
CEUR Workshop Proceedings
ISSN 1613-0073
http://ceur-ws.org/Vol-1591/
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’16) in Toruń, Poland, June 20–21, 2016. It is a
co-located event of
• Petri Nets 2016 – the 37th International Conference on Applications and
Theory of Petri Nets and Concurrency and
• ACSD 2016 – the 16th International Conference on Application of Con-
currency to System Design.
More information about the workshop can be found at
http://www.informatik.uni-hamburg.de/TGI/events/pnse16/
For the successful realization 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 modeling, validation and verification. Their popularity
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, colored Petri nets
and extensions) in the formal process of software engineering, covering mod-
eling, validation and verification, is presented as well as their application and
tools supporting the disciplines mentioned above.
We have chosen Gabriele Taentzer and Yann Thierry-Mieg as invited
speakers. We received twenty-three high-quality contributions. The program
committee has accepted eleven of them for full presentation. Four papers were
accepted as short presentations, two as short papers and one as poster pre-
sentation.
The international program committee was supported by the valued work
of David Mosteller, Camille Coti, Dimitri Racordon, Yann Ben Maissa, Alban
Linard, Thomas Wagner, Maciej Szreter, Benjamin Meis, Michał Knapik as
additional reviewers. Their work is highly appreciated.
Furthermore, we would like to thank our colleagues in the local organization
team at the Nicolaus Copernicus University in Toruń for their support. With-
out the enormous efforts of authors, reviewers, PC members and the organi-
zational team, this workshop would not provide such an interesting booklet.
Thanks!
Lawrence Cabac, Lars Michael Kristensen, Heiko Rölke
Hamburg, June 2016
6 PNSE’16 – Petri Nets and Software Engineering
Program Committee
Kamel Barkaoui (France)
Robin Bergenthum (Germany)
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)
Susanna Donatelli (Italy)
Giuliana Franceschinis (Italy)
Nicolas Guelfi (Luxembourg)
Stefan Haar (France)
Kunihiko Hiraishi (Japan)
Peter Kemper (USA)
Ekkart Kindler (Denmark)
Hanna Klaudel (France)
Michael Köhler-Bußmeier (Gemany)
Radek Koci (Czech republic)
Maciej Koutny (United Kingdom)
Lars Kristensen (Norway) (Chair)
Łukasz Mikulski (Poland)
Daniel Moldt (Germany)
Berndt Müller (Great Britain)
Wojciech Penczek (Poland)
Laure Petrucci (France)
Lucia Pomello (Italy)
Heiko Rölke (Germany) (Chair)
Yann Thierry-Mieg (France)
Henricus M.W. (Eric) Verbeek (Netherlands)
Jan Martijn van der Werf (Netherlands)
Karsten Wolf (Germany)
Preface 7
Preface BioPPN
This volume contains the peer-reviewed papers accepted for BioPPN 2016 –
the 7th International Workshop on Biological Processes & Petri Nets held on
June 20, 2015 in Toruń as satellite event of PETRI NETS 2016 and ACSD
2016.
The workshop had been organised to provide a platform for researchers
aiming at fundamental research and real life applications of Petri nets and
other concurrency models in Systems and Synthetic Biology. Systems and
Synthetic Biology are full of challenges and open issues, with adequate mod-
elling and analysis techniques being one of them. The need for appropriate
mathematical and computational modelling tools is widely acknowledged.
Petri nets offer a family of related models, which can be used as umbrella
formalism – models may share network structure, but vary in their kinetic
details. This undoubtedly contributes to bridging the gap between different
formalisms, and helps to unify diversity. Thus, Petri nets have proved their
usefulness for the modelling, analysis, and simulation of a diversity of biolog-
ical networks, covering qualitative, stochastic, continuous and hybrid models.
The deployment of Petri nets to study biological applications has not only sup-
ported the development of original models, but has also motivated research
of formal foundations.
The workshop was opened by an invited talk on Quasi-Steady State Petri
Nets given by Andrzej M Kierzek, Head of Systems Modeling, Simcyp a Cer-
tara company, Sheffield, UK and Visiting Professor of Systems Biology, Fac-
ulty of Health and Medical Sciences, University of Surrey, UK.
In addition, there was a Poster Session, and each poster was briefly intro-
duced by a short talk.
Each submission was reviewed by up to eight program committee members,
supported by an external subreviewer, followed by an intensive and thorough
discussion. The list of reviewers comprised 16 professionals of the field coming
from 9 different countries and writing in total 25 reviews, most of them of
substantial length. The programme committee finally decided to accept two
papers, involving 3 authors coming from two different countries, and three
posters, with authors all coming from Poland, the hosting country. The two
full papers got substantially improved in their final version – credits go to the
detailed reviews.
For more details see the workshop’s website
http://www-dssz.informatik.tu-cottbus.de/BME/BioPPN2016.
June 12, 2016 Anna Gambin
Cottbus Monika Heiner
8 PNSE’16 – Petri Nets and Software Engineering
Program Committee BioPPN
Gianfranco Balbo University of Torino, Computer Science Depart-
ment, Italy
Marco Becutti University of Torino, Computer Science Depart-
ment, Italy
Rainer Breitling University of Manchester, Manchester Institute of
Biotechnology, UK
Ming Chen Zhejiang University, College of Life Sciences,
Department of Bioinformatics, China
Piotr Formanowicz Poznan University of Technology & Polish
Academy of Sciences, Poland
Anna Gambin University of Warsaw, Division of Mathematics,
Informatics and Mechanics, Computational Biol-
ogy Group, Poland
David Gilbert Brunel University, Centre for Systems and Syn-
thetic Biology, UK
Simon Hardy Université Laval, Institut universitaire en santé
mentale de Québec, Canada
Monika Heiner Brandenburg University of Technology Cottbus-
Senftenberg, Computer Science Institute, Ger-
many
Mostafa Herajy Port Said University, Mathematics and Computer
Science Department, Egypt
Peter Kemper College of William and Mary, Department of Com-
puter Science, USA
Hanna Klaudel Universite d’Evry-Val d’Essonne, IBISC, F
Michal Komorowski Polish Academy of Sciences, Institute of Funda-
mental Technological Research, Division of Mod-
elling in Biology and Medicine, Poland
Chen Li Zhejiang University, School of Medicine, Center for
Genetic & Genomic Medicine, China
Fei Liu Harbin Institute of Technology, Control and Sim-
ulation Center, China
Wolfgang Marwan Otto von Guericke University Magdeburg &
Magdeburg Centre for Systems Biology, Germany
Hiroshi Matsuno Yamaguchi University, Graduate School of Science
and Engineering, Japan
Annegret K. Wagler Université Blaise Pascal (Clermont-Ferrand II),
Faculty of Sciences and Technology
Contents
Part I Invited Talks
Model-Driven Development of Mobile Applications: Towards
Context-Aware Apps of High Quality
Gabriele Taentzer and Steffen Vaupel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
Bridging the Gap Between Formal Methods and Software
Engineering Using Model-based Technology
Yann Thierry-Mieg . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
Part II Long Presentations
Time in Structured Occurrence Nets
Anirban Bhattacharyya, Bowen Li and Brian Randell . . . . . . . . . . . . . . . . . 35
Formal Modelling and Analysis of Distributed Storage
Systems
Jordan de la Houssaye, Franck Pommereau and Philippe Deniel . . . . . . . . 56
Introducing Refactoring for Reference Nets
Max Friedrich and Daniel Moldt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
Verification of Nested Petri Nets Using an Unfolding
Approach
Irina A. Lomazova and Vera O. Ermakova . . . . . . . . . . . . . . . . . . . . . . . . . . 93
Practical Use of Coloured Petri Nets for the Design
and Performance Assessment of Distributed Automation
Architectures
Moulaye Ndiaye, Jean-François Pétin, Jean-Philippe Georges and
Jacques Camerini . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
12 Contents
Kleene Theorem for Labelled Free Choice Nets without
Distributed Choice
Ramchandra Phawade . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132
Distributed Change Region Detection in Dynamic Evolution
of Fragmented Processes
Ahana Pradhan and Rushikesh K. Joshi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
Extending Renew’s Algorithms for Distributed Simulation
Michael Simon and Daniel Moldt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173
Model-based Development for MAC Protocols in Industrial
Wireless Sensor Networks
Admar Ajith Kumar Somappa and Kent Inge Fagerland Simonsen . . . . . . 193
Stubborn Set Intuition Explained
Antti Valmari and Henri Hansen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213
Decomposed Replay Using Hiding and Reduction
Henricus M.W. Verbeek . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233
Part III Short Presentations
Formally Proving and Enhancing a Self-Stabilising Distributed
Algorithm
Camille Coti, Charles Lakos and Laure Petrucci . . . . . . . . . . . . . . . . . . . . . 255
Refining the Quick Fix for the Petri Net Modeling Tool
Renew
Jan Hicken, Michael Haustermann and Daniel Moldt . . . . . . . . . . . . . . . . . 275
Layered Data: a Modular Formal Definition without
Formalisms
Alban Linard, Benoît Barbot, Didier Buchs, Maximilien Colange,
Clément Démoulins, Lom Messan Hillah and Alexis Martin . . . . . . . . . . . 287
From eHornets to Hybrid Agent and Workflow Systems
Thomas Wagner, Daniel Moldt and Michael Köhler-Bußmeier . . . . . . . . . 307
Part IV Short Papers
A Framework for Fast Congestion Detection in Wireless
Sensor Networks Using Clustering and Petri-Net-based
Verification
Khanh Le, Thang Bui, Tho Quan and Laure Petrucci . . . . . . . . . . . . . . . . . 329
Contents 13
CSCB Tools: A Tool to Synthesize Pareto Optimal State
Machine Models from Choreography Using Petri Nets
Toshiyuki Miyamoto . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 335
Part V Poster Presentation
Case Studies of the Renew Meta-Modeling and Transformation
Framework
David Mosteller, Michael Haustermann . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 343
Part VI BioPPN Papers
Analysis of the Signal Transduction Dynamics Regulating
mTOR with Mathematical Modeling, Petri Nets and Dynamic
Graphs
Simon V. Hardy and Mathieu Pagé Fortin . . . . . . . . . . . . . . . . . . . . . . . . . . 347
Discrete-Time Leap Method for Stochastic Simulation
Christian Rohr . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 362