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.

Bernardinello, L., Lomazova, I., Nesterov, R., Pomello, L. (2020). Property-Preserving transformations of elementary net systems based on morphisms. In CEUR Workshop Proceedings (pp.49-67). CEUR-WS.

Property-Preserving transformations of elementary net systems based on morphisms

Bernardinello L.
;
Nesterov R.
;
Pomello L.
2020

Abstract

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.
paper
Abstraction; Morphisms; Petri nets; Refinement; Transformations
English
2020 International Workshop on Petri Nets and Software Engineering, PNSE 2020
2020
CEUR Workshop Proceedings
2020
2020
2651
49
67
http://ceur-ws.org/Vol-2651/paper4.pdf
none
Bernardinello, L., Lomazova, I., Nesterov, R., Pomello, L. (2020). Property-Preserving transformations of elementary net systems based on morphisms. In CEUR Workshop Proceedings (pp.49-67). CEUR-WS.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/295858
Citazioni
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
Social impact