Proceedings of the International Workshop on P etri N ets and S oftware E ngineering PNSE'13

-

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 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’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

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 becoming increasingly popular in this area, as they provide a uniform language supporting the tasks of modelling, 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, 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:

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 appreciated.

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 organizational team this workshop wouldn’t provide such an interesting booklet.

Thank you,

Daniel Moldt and Heiko Rölke

Hamburg, June 2013

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

Petri Nets as a Means to Validate an Architecture for Time

Aware Systems

Francesco Fiamberti, Daniela Micucci and Francesco Tisato . . . . . . . . . . . 117

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

References