International Workshop on Biological Processes and Petri Nets
including papers of
Editors: Lawrence Cabac,
Lars Michael Kristensen,
Heiko Rölke Proceedings of the International Workshop on
Petri Nets and Software Engineering
PNSE’16 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 permitted only for private and academic purposes. This volume is published and copyrighted by its editors. 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 Concurrency 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 becoming 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 modeling, 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 presentation.
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. Without the enormous efforts of authors, reviewers, PC members and the organizational team, this workshop would not provide such an interesting booklet. Thanks! (Chair) (Chair) (Chair)
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 modelling 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 biological networks, covering qualitative, stochastic, continuous and hybrid models. The deployment of Petri nets to study biological applications has not only supported 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 Certara company, Sheffield, UK and Visiting Professor of Systems Biology, Faculty of Health and Medical Sciences, University of Surrey, UK.
In addition, there was a Poster Session, and each poster was briefly introduced 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. Anna Gambin Monika Heiner
Gianfranco Balbo Marco Becutti Rainer Breitling Ming Chen Piotr Formanowicz Anna Gambin David Gilbert Simon Hardy Monika Heiner Mostafa Herajy Peter Kemper Hanna Klaudel Michal Komorowski Chen Li Fei Liu Wolfgang Marwan Hiroshi Matsuno Annegret K. Wagler University of Torino, Computer Science Department, Italy University of Torino, Computer Science Department, Italy University of Manchester, Manchester Institute of Biotechnology, UK Zhejiang University, College of Life Sciences, Department of Bioinformatics, China Poznan University of Technology & Polish Academy of Sciences, Poland University of Warsaw, Division of Mathematics, Informatics and Mechanics, Computational Biology Group, Poland Brunel University, Centre for Systems and Synthetic Biology, UK Université Laval, Institut universitaire en santé mentale de Québec, Canada Brandenburg University of Technology CottbusSenftenberg, Computer Science Institute, Germany Port Said University, Mathematics and Computer Science Department, Egypt College of William and Mary, Department of Computer Science, USA Universite d’Evry-Val d’Essonne, IBISC, F Polish Academy of Sciences, Institute of Fundamental Technological Research, Division of Modelling in Biology and Medicine, Poland Zhejiang University, School of Medicine, Center for Genetic & Genomic Medicine, China Harbin Institute of Technology, Control and Simulation Center, China Otto von Guericke University Magdeburg & Magdeburg Centre for Systems Biology, Germany Yamaguchi University, Graduate School of Science and Engineering, Japan Université Blaise Pascal (Clermont-Ferrand II), Faculty of Sciences and Technology
Gabriele Taentzer and Steffen Vaupel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Bridging the Gap Between Formal Methods and Software Engineering Using Model-based Technology Yann Thierry-Mieg . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
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 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
Antti Valmari and Henri Hansen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213 Decomposed Replay Using Hiding and Reduction Henricus M.W. Verbeek . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233
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
Khanh Le, Thang Bui, Tho Quan and Laure Petrucci . . . . . . . . . . . . . . . . . 329 CSCB Tools: A Tool to Synthesize Pareto Optimal State Machine Models from Choreography Using Petri Nets Toshiyuki Miyamoto . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 335
David Mosteller, Michael Haustermann . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 343
Simon V. Hardy and Mathieu Pagé Fortin . . . . . . . . . . . . . . . . . . . . . . . . . . 347 Discrete-Time Leap Method for Stochastic Simulation Christian Rohr . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 362