Transpilation of Petri-nets into B | SpringerLink
Skip to main content
Springer Nature Link
Log in

Transpilation of Petri-nets into B

Shallow and Deep Embeddings

  • Conference paper
  • First Online:
Rigorous State-Based Methods (ABZ 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14759))

Included in the following conference series:

  • 211 Accesses

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 8464
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 9437
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Robot manip: https://mcc.lip6.fr/2024/pdf/RobotManipulation-form.pdf

    Satellite memory: https://mcc.lip6.fr/2024/pdf/SatelliteMemory-form.pdf

    Smart Home: https://mcc.lip6.fr/2024/pdf/SmartHome-form.pdf.

References

  1. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)

    Book  Google Scholar 

  2. Amparore, E., et al.: Presentation of the 9th edition of the model checking contest. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 50–68. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_4

    Chapter  Google Scholar 

  3. AtelierB. http://www.atelierb.eu/en/. Accessed 27 May 2021

  4. Attiogbé, C.: Semantic embedding of Petri nets into Event-B. In: Integration of Model-based Formal Methods Tools, Dusseldorf, Germany (2009)

    Google Scholar 

  5. Bendraou, R., Combemale, B., Crégut, X., Gervais, M.P.: Definition of an eXecutable SPEM 2.0. In: 14th Asia-Pacific Software Engineering Conference (APSEC), Nagoya, Japan, pp. 390–397. IEEE CS Press (2007)

    Google Scholar 

  6. Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA - construction of abstract state spaces for Petri nets and time Petri nets. Int. J. Prod. Res. 42(14), 2741–2756 (2004). https://doi.org/10.1080/00207540412331312688

    Article  Google Scholar 

  7. Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend, 2nd edn. Packt Publishing (2016)

    Google Scholar 

  8. Bobbio, A.: System modelling with Petri nets. In: Colombo, A.G., de Bustamante, A.S. (eds.) Systems Reliability Assessment, pp. 103–143. Springer, Netherlands, Dordrecht (1990). https://doi.org/10.1007/978-94-009-0649-5_6

    Chapter  Google Scholar 

  9. Bon, P., Collart-Dutilleul, S.: From a solution model to a B model for verification of safety properties. J. Univers. Comput. Sci. 19(1), 2–24 (2013)

    Google Scholar 

  10. Boulton, R.J., Gordon, A., Gordon, M.J.C., Harrison, J., Herbert, J., Tassel, J.V.: Experience with embedding hardware description languages in HOL. In: Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pp. 129–156. North-Holland Publishing Co., NLD (1992)

    Google Scholar 

  11. Distefano, S., Scarpa, M., Puliafito, A.: From UML to Petri nets: the PCM-based methodology. IEEE Trans. Softw. Eng. 37(1), 65–79 (2011). https://doi.org/10.1109/TSE.2010.10

    Article  Google Scholar 

  12. Dumas, M., García-Bañuelos, L.: Process mining reloaded: event structures as a unified representation of process models and event logs. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 33–48. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19488-2_2

    Chapter  Google Scholar 

  13. Eclipse: Acceleo (2012). http://www.eclipse.org/acceleo/

  14. Hartmann, T., Sadilek, D.A.: Undoing operational steps of domain-specific modeling languages. In: Proceedings of the 8th OOPSLA Workshop on Domain-Specific Modeling (DSM 2008) - University of Alabama at Birmingham (2008)

    Google Scholar 

  15. Hillah, L.M., Kordon, F., Petrucci, L., Trèves, N.: PNML framework: an extendable reference implementation of the Petri net markup language. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 318–327. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13675-7_20

    Chapter  Google Scholar 

  16. Idani, A.: Dependability of model-driven executable DSLs. In: Muccini, H., et al. (eds.) ECSA 2020. CCIS, vol. 1269, pp. 358–373. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-59155-7_27

    Chapter  Google Scholar 

  17. Idani, A.: Meeduse: a tool to build and run proved DSLs. In: Dongol, B., Troubitsyna, E. (eds.) IFM 2020. LNCS, vol. 12546, pp. 349–367. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-63461-2_19

    Chapter  Google Scholar 

  18. Idani, A.: Formal model-driven executable DSLs: application to Petri-nets. Int. NASA J. Innov. Syst. Softw. Eng. (ISSE) 18(4), 543–566 (2022). https://doi.org/10.1007/s11334-021-00408-4

    Article  Google Scholar 

  19. Idani, A., Ledru, Y., Vega, G.: Alliance of model driven engineering with a proof-based formal approach. Int. NASA J. Innov. Syst. Softw. Eng. (ISSE) 16(3) (2020)

    Google Scholar 

  20. Idani, A., Vega, G., Leuschel, M.: Applying formal reasoning to model transformation: the Meeduse solution. In: Proceedings of the 12th Transformation Tool Contest, co-located with STAF 2019, Software Technologies: Applications and Foundations. CEUR Workshop Proceedings, vol. 2550, pp. 33–44 (2019)

    Google Scholar 

  21. Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I., Valduriez, P.: ATL: A QVT-like transformation language. In: Companion to the 21st ACM SIGPLAN Symposium on Object-oriented Programming Systems, Languages, and Applications, OOPSLA 2006, pp. 719–720. ACM, New York (2006)

    Google Scholar 

  22. Kim, S.-K., David, C.: Formalizing the UML class diagram using object-Z. In: France, R., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 83–98. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-46852-8_7

    Chapter  Google Scholar 

  23. Korecko, S., Sobota, B.: Petri-nets to B-language transformation in software development. Acta Polytechnica Hungarica 11, 187–206 (2014)

    Google Scholar 

  24. Langer, P., Mayerhofer, T., Kappel, G.: Semantic model differencing utilizing behavioral semantics specifications. In: Dingel, J., Schulte, W., Ramos, I., Abrahão, S., Insfran, E. (eds.) MODELS 2014. LNCS, vol. 8767, pp. 116–132. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11653-2_8

    Chapter  Google Scholar 

  25. Lano, K., Clark, D., Androutsopoulos, K.: UML to B: formal verification of object-oriented models. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 187–206. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24756-2_11

    Chapter  Google Scholar 

  26. Lausdahl, K., Lintrup, H.K.A., Larsen, P.G.: Connecting UML and VDM++ with open tool support. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 563–578. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05089-3_36

    Chapter  Google Scholar 

  27. Leuschel, M.: Formal model-based constraint solving and document generation. In: Ribeiro, L., Lecomte, T. (eds.) SBMF 2016. LNCS, vol. 10090, pp. 3–20. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49815-7_1

    Chapter  Google Scholar 

  28. Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Softw. Tools Technol. Transfer (STTT) 10(2), 185–203 (2008)

    Article  Google Scholar 

  29. Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for Petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54–57. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_6

    Chapter  Google Scholar 

  30. Mayerhofer, T., Langer, P., Wimmer, M., Kappel, G.: xMOF: executable DSMLs based on fUML. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 56–75. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02654-1_4

    Chapter  Google Scholar 

  31. Meeduse. https://vasco.imag.fr/tools/meeduse/. Accessed 19 Feb 2024

  32. PNML. http://www.pnml.org. Accessed 27 May 2021

  33. Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: EMF: Eclipse Modeling Framework, 2nd edn. Addison-Wesley (2008)

    Google Scholar 

  34. The ePNK. http://www2.compute.dtu.dk/~ekki/projects/ePNK/index.shtml. Accessed 15 Dec 2020

  35. Wachsmuth, G.: Modelling the operational semantics of domain-specific modelling languages. In: Lämmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2007. LNCS, vol. 5235, pp. 506–520. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88643-3_16

    Chapter  Google Scholar 

  36. Wildmoser, M., Nipkow, T.: Certifying machine code safety: shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 305–320. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30142-4_22

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Univ. Grenoble Alpes, CNRS, LIG, 38000, Grenoble, France

    Akram Idani

Authors
  1. Akram Idani
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Akram Idani .

Editor information

Editors and Affiliations

  1. Department of Management, Information and Production Engineering, University of Bergamo, Bergamo, Italy

    Silvia Bonfanti

  2. Department of Management, Information and Production Engineering, University of Bergamo, Bergamo, Italy

    Angelo Gargantini

  3. Institut für Informatik, Heinrich-Heine-Universität, Düsseldorf, Germany

    Michael Leuschel

  4. Dipartimento di Informatica, Università degli Studi di Milano, Milan, Italy

    Elvinia Riccobene

  5. Department of Management, Information and Production Engineering, University of Bergamo, Bergamo, Italy

    Patrizia Scandurra

Ethics declarations

Competing Interests

The author(s) has no competing interests to declare that are relevant to the content of this manuscript.

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Idani, A. (2024). Transpilation of Petri-nets into B. In: Bonfanti, S., Gargantini, A., Leuschel, M., Riccobene, E., Scandurra, P. (eds) Rigorous State-Based Methods. ABZ 2024. Lecture Notes in Computer Science, vol 14759. Springer, Cham. https://doi.org/10.1007/978-3-031-63790-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-63790-2_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-63789-6

  • Online ISBN: 978-3-031-63790-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation