Semantic Embedding of Petri Nets into Event-B

TL;DR

This paper introduces a method to embed Petri nets into Event-B systems, allowing combined analysis and development by translating static structure and evolution semantics of Petri nets into B abstract systems.

Contribution

It provides a novel embedding technique that captures Petri nets' structure and behavior within Event-B, enabling integrated system modeling and analysis.

Findings

Embedding captures static structure via graph in B

Evolution semantics modeled with B events

Supports combined Petri net and Event-B analysis

Abstract

We present an embedding of Petri nets into B abstract systems. The embedding is achieved by translating both the static structure (modelling aspect) and the evolution semantics of Petri nets. The static structure of a Petri-net is captured within a B abstract system through a graph structure. This abstract system is then included in another abstract system which captures the evolution semantics of Petri-nets. The evolution semantics results in some B events depending on the chosen policies: basic nets or high level Petri nets. The current embedding enables one to use conjointly Petri nets and Event-B in the same system development, but at different steps and for various analysis.