International Workshop on Petri Nets and Software Engineering
Zaragoza, Spain, June 26-27, 2017
a satellite event of
Petri Nets 2017 and ACSD 2017
38th INTERNATIONAL CONFERENCE ON APPLICATION AND
THEORY OF PETRI NETS AND CONCURRENCY
17th INTERNATIONAL CONFERENCE ON
APPLICATION OF CONCURRENCY TO SYSTEM DESIGN
Contact e-mail: pnse17_at_informatik_dot_uni-hamburg_dot_de
Registration & Accommodation
Please register for the PNSE'17 workshop at the
Petri Nets 2017 Registration
Information about how to reach the workshop / conference site and
about hotels can be found at the
Petri Nets 2017 Venue pages.
||José Jean-Paul Zanlucchi de Sousa Tavares, Rodrigo Hiroshi Murofushi, Lucas Henriques Silva and Gustavo Rezende Silva
||Petri Net Inside RFID Database Integrated with RFID Indoor Positioning System for Mobile Robots Position Control
||Soumia Mancer and Hammadi Bennoui
||Coloured Petri Nets Based Diagnosis on Causal Models
||Elvio Gilberto Amparore, Susanna Donatelli, Marco Beccuti, Giulio Garbi and Andrew Miner
||Decision Diagrams for Petri Nets: which Variable Ordering?
||Vladimir A. Bashkin
||On the Resource Equivalences in Petri nets with Invisible Transitions
||Thomas Hildebrandt (Invited Speaker)
||Modelling & Mining Event-based Concurrent Declarative Processes as Dynamic Condition Response Graphs
||D. Dahmani, M.C. Boukala, H. Mountassir and S. Chouali
||Compatibility Control of Asynchronous Communicating Systems with Unbounded Buffers
||Karima Ennaoui, Lhouari Nourine and Farouk Toumani
||Complexity Aspects of Web Services Composition
||Simona Bernardi, Raúl Piracés Alastuey, Alejandro Solanas Bonilla and Raquel Trillo-Lado
||Towards a Systematic Model-driven Approach for the Detection of Web Threats and Use Cases
||Lars M. Kristensen and Gabriele Taentzer and Steffen Vaupel
||Towards Verification of Connection-Aware Transaction Models for Mobile Applications
||João Paulo Da Silva Fonseca and Jose Jean-Paul Zanlucchi de Souza Tavares
||Petri Net with RFID Distributed Database for Autonomous Search and Rescue in Tracks and Crossings
||Poster Presentation + Coffee Break
||Julia Padberg (Invited Speaker)
||Verification of Reconfigurable Petri Nets
||José Ángel Bañares (Invited Speaker)
||Model-Driven Development of Performance Sensitive Cloud Native Streaming Applications
||Pascale Möller, Michael Haustermann, David Mosteller, Dennis Schmitz
||Simulating Multiple Formalisms Concurrently Based on Reference Nets
||Rowland Pitts and Hassan Gomaa
||Modeling Reusable Concurrent Passive Entity Objects in Colored Petri Nets
||A Tool Chain for Test-driven Development of Reference Net Software Components in the Context of CAPA Agents
||Oscar Urra and Sergio Ilarri
||Modeling Mobile Agents in Vehicular Networks
||Rui Wang, Lars Michael Kristensen, Hein Meling and Volker Stolz
||Application of Model-based Testing on a Quorum-based Distributed Storage
||Anna Gogolińska, Łukasz Mikulski and Marcin Piątkowski
||GPU Computations and Memory Access Model Based on Petri Nets
- José Ángel Bañares
(University of Zaragoza):
Model-Driven Development of Performance
Sensitive Cloud Native Streaming Applications
The number of applications that process data in a stream basis has increased significantly over recent years due to the proliferation of sensors. Additionally, in cyber-physical systems, physical and software components are deeply intertwined, adding the ability to act on the environment.
In many cases, cloud resources are used for the processing, exploiting their flexibility, but these sensor streaming applications often need to support operational and control actions that have real-time and low-latency requirements that go beyond the cost effective and flexible solutions supported by cloud platforms. The development of these applications cannot be delegated to the magical properties of frameworks and services that promise simple solutions, hiding the inherent underlying complexity of cloud resources. It raises the difficulty of developing complex streaming processing in the cloud and highlights the need for a suitable developing methodology. Moreover, during the developing lifecycle, a number of facets have to be considered such as the design of functional parallel solutions, the impact of a target cloud platform that exhibits different degrees of performance variability, or the need for more complex performance requirement support. This talk will present our experiences in developing Petri Net models for performance sensitive cloud applications thus leveraging the use of formal models in complex scenarios.
- Julia Padberg
Verification of Reconfigurable Petri Nets
We introduce a family of modeling techniques consisting
of Petri nets together with a set of rules. For reconfigurable Petri
nets, e.g. in  not only the follower marking can be computed but also
the structure can be changed by rule application to obtain a new net.
Motivation is the observation that in increasingly many application areas the
underlying system has to be dynamic in a structural sense.
Complex coordination and structural adaptation at run-time (e.g. mobile ad-hoc
networks, dynamic hardware reconfiguration,
communication spaces, ubiquitous computing) are main features that need
to be modelled adequately. The distinction between the net behaviour and
the dynamic change of its net structure is the characteristic feature that makes reconfigurable Petri nets so suitable for modeling systems with dynamic structures.
For rule-based modification of Petri nets we use the framework of net
transformations that is inspired by graph transformation systems .
The basic idea behind net transformation is the stepwise modification of Petri nets
by given rules. The rules present a rewriting of nets where the
left-hand side is replaced by the right-hand side.
The abstract semantics we introduce in  is a graph with nodes that consist of isomorphism classes of the net structure and an isomorphism class of the current marking. Arcs between these nodes represent computation steps being either a transition firing or a
direct transformation. Based on this semantics we can define properties and model-check these properties.
Model checking is a widely used technique to prove properties such as liveness, deadlock or safety
for a given model. Here we present model checking of reconfigurable Petri nets [7,6].
The main task is to flatten the two levels of dynamic behavior that reconfigurable nets provide,
the firing of transitions on the one hand and the transformation of the nets on the other hand.
We show how to translate a reconfigurable net into Maude modules . Maude's LTL model-checker
is then used to verify properties of these modules. The correctness of this conversion is proven as
the corresponding labelled transitions systems are bisimular.
In an ongoing example reconfigurable Petri nets are used to model and to verify partial dynamic
reconfiguration of field programmable gate arrays using the tool ReconNet ( or see https://reconnetblog.wordpress.com).
Some of the best papers from the workshop will be invited for publication in a volume of the journal sub line of Lecture Notes in Computer Science entitled
"Transactions on Petri Nets and Other Models of Concurrency" (ToPNoC)
The papers are expected to be thoroughly revised and they will go through a totally new round of reviewing as is standard practice for journal papers.
Papers from previous instances of this workshop
made it into ToPNoC volumes in the Springer LNCS series (volumes
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 workshop PNSE'17 (Petri nets and Software Engineering) will take place as a satellite event of Petri Nets 2017 and ACSD 2017.
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, will be presented as well as their application and tools supporting the disciplines mentioned above.
We welcome contributions describing original research in topics related to Petri nets in combination with software engineering, addressing open problems or presenting new ideas regarding
the relation of Petri nets and software engineering.
Furthermore we look for surveys addressing open problems and new applications of Petri nets.
Topics of interest include but are not limited to:
representation of formal models by intuitive modeling concepts
guidelines for the construction of system models
process-, service-, state-, event-, object- and agent-oriented approaches
adaption, integration, and enhancement of concepts from other
views and abstractions of systems
modeling software landscapes
web service-based software development
Validation and Execution
simulation, observation, animation
code generation and execution
testing and debugging
structural methods (e.g. place invariants, reduction rules)
results for structural subclasses of nets
relations between structure and behavior
state space based approaches
efficient model checking
assertional and deductive methods (e.g. temporal logics)
process algebraic methods
applications of category theory and linear logic
Application of Petri nets in Software Engineering, in particular the
use of Petri nets in the domains of
- flexible manufacturing,
- big data,
- cyper-physical systems,
- cloud computing,
- distributed systems,
- workflow management and
- embedded systems.
Tools in the fields mentioned above
The workshop proceedings for PNSE'17 will be available online at CEUR (available from June 30.).
CEUR-WS.org as Volume 1846.
- Elvio Amparore ( Università degli Studi di Torino, Italy)
- Kamel Barkaoui (Conservatoire National des Arts et Métiers, France)
- Robin Bergenthum (University of Hagen, Germany)
- Didier Buchs (University of Geneva, Switzerland)
- Lawrence Cabac (University of Hamburg, Germany) (Co-Chair)
- Piotr Chrzastowski-Wachtel (University of Warsaw, Poland)
- Gianfranco Ciardo (Iowa State University, USA)
- José-Manuel Colom (University of Zaragoza, Spain)
- Jörg Desel (University of Hagen, Germany)
- Raymond Devillers (Université Libre de Bruxelles, Belgium)
- Giuliana Franceschinis (Università del Piemonte Orientale, Italy)
- Nicolas Guelfi (University of Luxembourg)
- Stefan Haar (ENS Cachan, France)
- Serge Haddad (ENS Cachan, France)
- Xudong He (Florida International University, USA)
- Kunihiko Hiraishi (Japan Advanced Institute of Science and Technology, Japan)
- Gabriel Juhás (Slovak University of Technology Bratislava, Slovakia)
- Peter Kemper (College of William and Mary, USA)
- Astrid Kiehn (IIT Mandi, India)
- Hanna Klaudel (Université d'Evry-Val d'Essonne, France)
- Michael Köhler-Bußmeier (University of Applied Science Hamburg, Gemany)
- Radek Koci (University of Brno, Czech republic)
- Maciej Koutny (Newcastle University, United Kingdom)
- Lars Kristensen (Bergen University College, Norway)
- Robert Lorenz (University of Augsburg, Germany)
- Łukasz Mikulski (Nicolaus Copernicus University, Toruń, Poland)
- Daniel Moldt (University of Hamburg, Germany) (Co-Chair)
- Berndt Müller (University of Glamorgan, UK)
- Wojciech Penczek (University of Podlasie, Poland)
- Laure Petrucci (University Paris Nord, France)
- Lucia Pomello (Università degli Studi di Milano-Bicocca, Italy)
- Heiko Rölke (DIPF, Germany) (Co-Chair)
- Yann Thierry-Mieg (University P. & M. Curie, LIP 6, France)
- P.S. Thiagarajan (Harvard Medical School, USA)
- H.M.W. Eric Verbeek (Eindhoven University, Netherlands)
- Karsten Wolf (University of Rostock, Germany)