Partitioning of Petri net models amenable for Distributed Execution

Considering the area of hardware-software co-design of embedded systems, techniques for system model partitioning into components are a major concern. If one uses Petri nets as the system-level specification language, it is mandatory to have specific mechanisms to produce sub-models from the whole system model; each sub-model will be associated with one component. This paper uses a running example to present a Petri net operation, called split, able to decompose a Petri net model into disjoint sub-models, based on the definition of a valid cutting set. Each sub-model is associated with a component with autonomous execution. After, modeling of communication channels among components are considered allowing the construction of the whole implemented system model and supporting verification of properties of the whole system.