Book
Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020)
Trading systems have become sophisticated multi-agent in-frastructures with complex development cycles. This is why the financialindustry constantly seeks for novel approaches to design and validate these systems. We propose the use of models to support such tasks. On the one hand, these models need to describe how objects (e.g., ordersto buy/sell securities) are shared by the system and traders. On the other hand, being a dynamic multi-agent system, models of trading systems should have a clear structure, describing how participants interact between each other. In this paper, we address these requirements, integrating notions of various Petri net extensions. In particular, we discuss modeling capabilities/limitations of each extension, and we propose to integrate them into a single approach, allowing for comprehensive modeling of different trading system components.
Structural transformations that preserve properties of formal models of concurrent systems make their verification easier. We define structural transformations that allow to abstract and refine elementary net systems. Relations between abstract models and their refinements are formalized using morphisms. Transformations proposed in this paper induce morphisms between elementary net systems as well as preserve their behavioral properties. We also show application of the proposed transformations to the construction of a correct composition of interacting workflow net components.
These are the proceedings of the International Workshop on Petri Nets and Software Engineering (PNSE’13) and the International Workshop on Modeling and Business Environments (ModBE’13) in Milano, Italy, June 24–25, 2013. These are co-located events of Petri Nets 2013, the 34th international conference on Applications and Theory of Petri Nets and Concurrency.
PNSE'13 presents 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, as well as their application and tools supporting the disciplines mentioned above.
ModBE’13 provides a forum for researchers from interested communities to investigate, experience, compare, contrast and discuss solutions for modeling in business environments with Petri nets and other modeling techniques.
This book constitutes the proceedings of the 37th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2016, held in Toruń, Poland, in June 2016. Petri Nets 2016 was co-located with the Application of Concurrency to System Design Conference, ACSD 2016. The 16 papers including 3 tool papers with 4 invited talks presented together in this volume were carefully reviewed and selected from 42 submissions. Papers presenting original research on application or theory of Petri nets, as well as contributions addressing topics relevant to the general field of distributed and concurrent systems are presented within this volume.
Measuring the value of IT is always a challenge for investors. Market share for service oriented Information Systems (IS) is constantly growing and it creates the demand for methods of measuring the value of SOA-based IS projects. This research is aimed at adopting existing IT Project assessment methods to this growing demand. The work proposes the method that considers the fact that SOA-based IS deployment and evolution could be split in separate flows, one per service. It will allow usage of individual discount rate values per service since project risk values should be different for different services. It should make project value assessment more accurate comparing to existing methods which use the single flow for the entire project. This research also proposes Real Options for calculating the flexibility fraction of the value. The developed method was verified using own simulation model. Both developed method and the simulation model were applied to value assessment of a real-world project.
Process mining is a relatively new field of computer science which deals with process discovery and analysis based on event logs. In this work we consider the problem of discovering workflow nets with cancellation regions from event logs. Cancellations occur in the majority of real-life event logs. In spite of huge amount of process mining techniques little has been done on cancellation regions discovery. We show that the state-based region algorithm gives labeled Petri nets with overcomplicated control flow structure for logs with cancellations. We propose a novel method to discover cancellation regions from the transition systems built on event logs and show the way to construct equivalent workflow net with reset arcs to simplify the control flow structure.
In this work we consider modeling of services with workflow modules, which are a subclass of Petri nets. The service compatibility problem is to answer the question, whether two Web services fit together, i.e. whether the composed system is sound. We study complementarity of service produced/consumed resources, that is a necessary condition for the service compatibility. Resources, which are produced/consumed by a Web service, are described as a multiset language. We define an algebra of multiset languages and present an algorithm for checking the conformance of resources for two given structured workflow modules.
Recent breakthroughs in process mining research make it possible to discover, analyze, and improve business processes based on event data. The growth of event data provides many opportunities but also imposes new challenges. Process mining is typically done for an isolated well-defined process in steady-state. However, the boundaries of a process may be fluid and there is a need to continuously view event data from different angles. This paper proposes the notion of process cubes where events and process models are organized using different dimensions. Each cell in the process cube corresponds to a set of events and can be used to discover a process model, to check conformance with respect to some process model, or to discover bottlenecks. The idea is related to the well-known OLAP (Online Analytical Processing) data cubes and associated operations such as slice, dice, roll-up, and drill-down. However, there are also significant differences because of the process-related nature of event data. For example, process discovery based on events is incomparable to computing the average or sum over a set of numerical values. Moreover, dimensions related to process instances (e.g. cases are split into gold and silver customers), subprocesses (e.g. acquisition versus delivery), organizational entities (e.g. backoffice versus frontoffice), and time (e.g., 2010, 2011, 2012, and 2013) are semantically different and it is challenging to slice, dice, roll-up, and drill-down process mining results efficiently.
Measuring the value of IT is always a challenge for investors. Market share for service oriented Information Systems (IS) is constantly growing and it creates the demand for methods of measuring the value of SOA-based IS projects. This research is aimed at adopting existing IT Project assessment methods to this growing demand. The work proposes the method that considers the fact that SOA-based IS deployment and evolution could be split in separate flows, one per service. It will allow using individual discounts rate values since project risk values should be different for different services. It should make project value assessment more accurate comparing to existing methods which use the single flow for the entire project. This research also proposes Real Options for calculating the flexibility fraction of the value. The developed method was verified using own simulation model. Both developed method and the simulation model were applied to value assessment of a real-world project.
To verify realtime properties of UML statecharts one may apply a UPPAAL, toolbox for model checking of realtime systems. One of the most suitable ways to specify an operational semantics of UML statecharts is to invoke the formal model of Hierarchical Timed Automata. Since the model language of UPPAAL is based on Networks of Timed Automata one has to provide a conversion of Hierarchical Timed Automata to Networks of Timed Automata. In this paper we describe this conversion algorithm and prove that it is correct w.r.t. UPPAAL query language which is based on the subset of Timed CTL.