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

These proceedings are published online with CEUR Workshop Proceedings (http:// CEUR-WS.org/, ISSN 1613-0073) as Volume 723. 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 Petru Nets and Software Engineering (PNSE’11) in Newcastle upon Tyne, United Kingdom, June 20–21, 2011. It is a co-located event of Petri Nets 2011, the 32nd international conference on Applications and Theory of Petri Nets and Concurrency, and ACSD 2011, the 11th International Conference on Application of Concurrency to System Design.

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, is presented as well as their application and tools supporting the disciplines mentioned above.

 The program committee consists of:

PNSE’11 – Petri Nets and Software Engineering We received 18 high-quality contributions. The program committee has accepted five of them for full presentation. Furthermore the committee accepted six papers as short presentations. Two contributions were submitted and accepted as posters.

The international program committee was supported by the valued work of Luca Bernardinello, Kent Inge Fagerland Simonsen, Elisabetta Mangioni, Artur Męski, Maciej Szreter, and Samir Tata as additional reviewers. Their work is highly appreciated.

Furthermore, we would like to thank the organizational teams of the Japan Advanced Institute of Science and Technology, Kanazawa, Japan and the University of Newcastle, Newcastle upon Tyne, U.K., for their general organizational support.

Without the enormous efforts of authors, reviewers, PC members and the organizational teams this workshop wouldn’t provide such an interesting booklet.

 Thanks! Michael Duvigneau, Daniel Moldt, and Kunihiko Hiraishi Newcastle, June 2011 Part I Invited Talks Unfolding Models of Asynchronous Systems: Applications to Analysis and Synthesis

Victor Khomenko . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

 Design, Modelling and Analysis of a Workflow Reconfiguration

Manuel Mazzara, Faisal Abouzaid, Nicola Dragon and Anirban Bhattacharyya . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

 Part II Long Presentations Efficient Implementation of Prioritized Transitions for High-level Petri Nets

Michael Westergaard and H.M.W. (Eric) Verbeek . . . . . . . . . . . . . . . . . . . . 27

 Modelling Local and Global Behaviour: Petri Nets and Event Coordination

Ekkart Kindler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

 Towards Verifying Parallel Algorithms and Programs using Coloured Petri Nets

Michael Westergaard . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

 Bounded Model Checking Approaches for Verification of Distributed Time Petri Nets

Artur Męski, Agata Półrola, Wojciech Penczek, Bożena WoźnaSzcześniak and Andrzej Zbrzezny . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72

 Extending PNML Scope: the Prioritised Petri Nets Experience

Lom-Messan Hillah, Fabrice Kordon, Charles Lakos and Laure Petrucci . 92

 Part III Short Presentations Specialisation and Generalisation of Processes

Christine Choppy, Jörg Desel and Laure Petrucci . . . . . . . . . . . . . . . . . . . . 109

 Integrating Verification into the PAOSE Approach

Marcin Hewelt, Thomas Wagner and Lawrence Cabac . . . . . . . . . . . . . . . . . 124

 Transitions as Transactions

Shengyuan Wang, Weiyi Wu, Yao Zhang and Yuan Dong . . . . . . . . . . . . . 136

 A Component Framework where Port Compatibility Implies Weak Termination

Debjyoti Bera, Kees M. van Hee, Michiel van Osch and Jan Martijn van der Werf . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152

 Improving the Development Tool Chain in the Context of Petri Net-Based Software Development

Tobias Betz, Lawrence Cabac and Matthias Güttler . . . . . . . . . . . . . . . . . . . 167

 On the use of Pragmatics for Model-based Development of Protocol Software

Kent Inge Fagerland Simonsen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179

 Part IV Poster Abstracts A Goal Based Approach on top of Petri Nets

Nejm Saadallah and Benoit Daireaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193

 PNTM – Integration of Petri Nets and Transactional Memory

Weiyi Wu, Yao Zhang, Shengyuan Wang and Yuan Dong . . . . . . . . . . . . . 196