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