ABCD: A User-Friendly Language for Formal Modelling and Analysis

  • Franck PommereauEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9698)


This paper presents an algebra of coloured Petri nets called the Asynchronous Box Calculus with Data, or abcd for short. abcd allows to model complex systems using a user-friendly and high-level syntax. In particular, parts of the model can be directly programmed in Python [21], which allows to embed complex computation and data values within a model. A compiler for abcd is shipped with the toolkit snakes [16, 18] and abcd has been used for years, which is quickly surveyed. This paper is the first complete and formal presentation of the language and its semantics. It also presents uses cases of abcd for the modelling and analysis of various systems.


Formal modelling High-level models Petri nets semantics 


  1. 1.
    Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Best, E., Devillers, R., Hall, J.G.: The box calculus: a new causal algebra with multi-label communication. In: Rozenberg, G. (ed.) Advances in Petri Nets 1992. LNCS, vol. 609, pp. 21–69. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  3. 3.
    Best, E., Devillers, R., Koutny, M.: Petri Net Algebra. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Best, E., Hopkins, R.P.: \(B(PN)^2\) - a basic Petri net programming notation. In: Bode, A., Reeve, M., Wolf, G. (eds.) PARLE 1993 Parallel Architectures and Languages Europe. LNCS, vol. 694, pp. 379–390. Springer, Heidelberg (1993)Google Scholar
  5. 5.
    Chaou, S., Utard, G., Pommereau, F.: Evaluating a peer-to-peer storage system in presence of malicious peers. In: Proceedings of HPCS 2011. IEEE Computer Society (2011)Google Scholar
  6. 6.
    Delaplace, F., Di Giusto, C., Giavitto, J.L., Klaudel, H., Spicher, A.: Activity networks with delays application to toxicity analysis. Technical report hal-01152719, I3S, Univ. Nice Sophia Antipolis (2015)Google Scholar
  7. 7.
    Di Guisto, C., Klaudel, H., Delaplace, F.: Systemic approach for toxicity analysis. In: Proceedings of BioPPN 2014. CEUR Workshop Proceedings, vol. 1159 (2014)Google Scholar
  8. 8.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Fronc, Ł., Duret-Lutz, A.: LTL model checking with Neco. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 451–454. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  10. 10.
    Gava, F., Pommereau, F., Guedj, M.: A BSP algorithm for on-the-fly checking CTL* formulas on security protocols. J. Supercomput. 69, 629–672 (2014)CrossRefGoogle Scholar
  11. 11.
    Kordon, F., Buchs, D., Garavel, H., Hillah, L.: MCC 2016 - models.
  12. 12.
    Kordon, F., Linard, A., Buchs, D., Colange, M., Evangelista, S., Fronc, Ł., Hillah, L.M., Lohmann, N., Paviot-Adet, E., Pommereau, F., Rohr, C., Thierry-Mieg, Y., Wimmel, H., Wolf, K. (eds.): Raw report on the model-checking contest at Petri nets 2012. CoRR arXiv:1209.2382, September 2012
  13. 13.
    Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)CrossRefGoogle Scholar
  14. 14.
    Parallel Systems Group, University of Oldenburg: The PEP tool.
  15. 15.
    Pommereau, F.: Model-checking with ABCD and Neco.
  16. 16.
    Pommereau, F.: The SNAKES toolkit. fpommereau/SNAKES/ with sources at
  17. 17.
    Pommereau, F.: Algebras of Coloured Petri Nets. Lambert Academic Publishing, Germany (2010)Google Scholar
  18. 18.
    Pommereau, F.: SNAKES: a flexible high-level Petri nets library. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 20115. LNCS, vol. 9115, pp. 254–265. Springer, Switzerland (2015)CrossRefGoogle Scholar
  19. 19.
    Sanjabi, S., Pommereau, F.: Modelling, verification, and formal analysis of security properties in a P2P system. In: Proceedings of COLSEC 2010. IEEE Digital Library, IEEE Computer Society (2010)Google Scholar
  20. 20.
    The Python Software Foundation: The Python tutorial.
  21. 21.
    The Python Software Foundation: Python website.

Copyright information

© Springer International Publishing Switzerland 2016

Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 2.5 International License (, which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.IBISCUniversity of ÉvryÉvry CedexFrance

Personalised recommendations