Editors: Daniel Moldt and Heiko Rölke Proceedings of the International Workshop on P etri N ets and S oftware E ngineering PNSE’13 University of Hamburg Department of Informatics These proceedings are published online by the editors as Volume 989 at CEUR Workshop Proceedings ISSN 1613-0073 http://ceur-ws.org/Vol-989 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’13) in Milano, Italy, June 24–25, 2013. It is a co-located event of Petri Nets 2013, the 34th international conference on Applications and Theory of Petri Nets and Concurrency. More information about the workshop can be found at http://www.informatik.uni-hamburg.de/TGI/events/pnse13/ 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: Wil van der Aalst (The Netherlands) Kamel Barkaoui (France) Didier Buchs (Switzerland) Lawrence Cabac (Germany) Piotr Chrzastowski-Wachtel (Poland) Gianfranco Ciardo (USA) José-Manuel Colom (Spain) Jörg Desel (Germany) Raymond Devillers (Belgium) Jorge C.A. de Figueiredo (Brasilia) Giuliana Franceschinis (Italy) Luís Gomes (Portugal) Stefan Haar (France) Serge Haddad (France) Xudong He (USA) Kees van Hee (The Netherlands) Thomas Hildebrandt (Danmark) Kunihiko Hiraishi (Japan) Vladimír Janoušek (Czech republic) Gabriel Juhás (Slovakia) Peter Kemper (USA) Astrid Kiehn (India) 10 PNSE’13 – Petri Nets and Software Engineering Hanna Klaudel (France) Radek Kočí (Czech republic) Fabrice Kordon (France) Maciej Koutny (United Kingdom) Lars Kristensen (Norway) Michael Köhler-Bußmeier (Germany) Johan Lilius (Finland) Robert Lorenz (Germany) Daniel Moldt (Germany) (Chair) Chun Ouyang (Australia) Wojciech Penczek (Poland) Laure Petrucci (France) Lucia Pomello (Italy) Heiko Rölke (Germany) (Chair) Catherine Tessier (France) H.M.W. (Eric) Verbeek (Netherlands) Karsten Wolf (Germany) There is one invited talk by Andrea Omicini and Stefano Mariani from Alma Mater Studiorum–Università di Bologna, Italy. We received 25 high-quality contributions. For each paper three to four reviews were made. The program committee has accepted six of them for full presentation. Furthermore the committee accepted six papers as short presentations and two short papers. Two more contributions were accepted as posters. The international program committee was supported by the valued work of Edmundo López Bóbeda, Görkem Kılınç, Reng Zeng, Benoît Barbot, Alexis Marechal and Artur Meski as additional reviewers. Their work is highly ap- preciated. Furthermore, we would like to thank our colleagues in the local organization team at the University of Milano Bicocca, Italy, 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 2013 Contents PNSE’13 Proceedings Part I PNSE’13: Invited Talk Coordination for Situated MAS: Towards an Event-driven Architecture Andrea Omicini and Stefano Mariani . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Part II PNSE’13: Long Presentations A Canonical Contraction for Safe Petri Nets Thomas Chatain and Stefan Haar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Symbolic verification of ECA rules Xiaoqing Jin, Yousra Lembachar and Gianfranco Ciardo . . . . . . . . . . . . . . 41 Soundness of Workflow Nets with an Unbounded Resource is Decidable Vladimir A. Bashkin and Irina A. Lomazova . . . . . . . . . . . . . . . . . . . . . . . . 61 Modeling Distributed Private Key Generation by Composing Petri Nets Luca Bernardinello, Görkem Kılınç, Elisabetta Mangioni and Lucia Pomello . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 Integrating Web Services in Petri Net-based Agent Applications Lawrence Cabac, Tobias Betz, Michael Duvigneau, Thomas Wagner and Matthias Wester-Ebbinghaus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 Petri Nets as a Means to Validate an Architecture for Time Aware Systems Francesco Fiamberti, Daniela Micucci and Francesco Tisato . . . . . . . . . . . 117 Part III PNSE’13: Short Presentations A Framework for Efficiently Deciding Language Inclusion for Sound Unlabelled WF-Nets Dennis Schunselaar, Eric Verbeek, Wil van der Aalst and Hajo A. Reijers135 Introducing Catch Arcs to Java Reference Nets Lawrence Cabac and Michael Simon . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 A System Performance in Presence of Faults Modeling Framework Using AADL and GSPNs Belhassen Mazigh and Kais Ben Fadhel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169 Coloured Petri Nets Refinements Christine Choppy, Laure Petrucci and Alfred Sanogo . . . . . . . . . . . . . . . . . . 187 Petri Nets-Based Development of Dynamically Reconfigurable Embedded Systems Tomáš Richta, Vladimír Janoušek and Radek Kočí . . . . . . . . . . . . . . . . . . . 203 Decomposing Replay Problems: A Case Study Eric Verbeek and Wil van der Aalst . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219 Part IV PNSE’13: Short Papers Building Petri Nets Tools around Neco Compiler Łukasz Fronc and Franck Pommereau . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 239 RT-Studio: A Tool for Modular Design and Analysis of Realtime Systems Using Interpreted Time Petri Nets Rachid Hadjidj and Hanifa Boucheneb . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 247 Part V PNSE’13: Poster Abstracts A Tool to Synthesize Intelligible State Machine Models from Choreography using Petri Nets Toshiyuki Miyamoto and Hiroyuki Oimura . . . . . . . . . . . . . . . . . . . . . . . . . . 257 Transforming Platform Independent CPN Models into Code for the TinyOS Platform: A Case Study of the RPL Protocol Vegard Veiset and Lars Michael Kristensen . . . . . . . . . . . . . . . . . . . . . . . . . . 259