Transpilation of Petri-nets into B - Université Grenoble Alpes
Communication Dans Un Congrès Année : 2024

Transpilation of Petri-nets into B

Résumé

Petri-nets and their variants (Place/Transition nets, High-Level Petri Nets, etc.) are widely used in the development of safety critical-systems. Their success is related to three major aspects: a formal semantics, a graphical syntax and the availability of verification tools. In our previous work we presented a new vision for the semantic definition of Petri-nets applying a Formal Model-Driven Engineering (FMDE) built on the B method. The approach is powered by Meeduse, a language workbench that we developed in order to formally instrument executable Domain-Specific Languages (xDSLs) by applying a deep embedding technique and the B method. However, because of the abstract nature of the underlying formal models, our deep embedding is suitable for the validation and verification activities at the design stage but not sufficient to generate code for target platforms. This paper advances our previous work with a shallow embedding technique taking benefit of the B method tools in order to safely synthesize executable Petri-net controllers that can be embedded in target platforms.
Fichier non déposé

Dates et versions

hal-04730397 , version 1 (10-10-2024)

Identifiants

Citer

Akram Idani. Transpilation of Petri-nets into B. ABZ: International Conference on Rigorous State-Based Methods, Jun 2024, Bergamo, Italy. pp.80-98, ⟨10.1007/978-3-031-63790-2_5⟩. ⟨hal-04730397⟩
1 Consultations
0 Téléchargements

Altmetric

Partager

More