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.