Performance Evaluation of the NDN Data Plane Using Statistical Model Checking

  • Siham Khoussi
  • Ayoub Nouri
  • Junxiao Shi
  • James Filliben
  • Lotfi Benmohamed
  • Abdella Battou
  • Saddek BensalemEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11781)


Named Data Networking (NDN) is an emerging internet architecture that addresses weaknesses of the Internet Protocol (IP). Since Internet users and applications have demonstrated an ever-increasing need for high speed packet forwarding, research groups have investigated different designs and implementations for fast NDN data plane forwarders and claimed they were capable of achieving high throughput rates. However, the correctness of these statements is not supported by any verification technique or formal proof. In this paper, we propose using a formal model-based approach to overcome this issue. We consider the NDN-DPDK prototype implementation of a forwarder developed at the National Institute of Standards and Technology (NIST), which leverages concurrency to enhance overall quality of service. We use our approach to improve its design and to formally demonstrate that it can achieve high throughput rates.


NDN SMC Model-based design Networking 


  1. 1.
    Brown, B.: Cisco, UCLA & more launch named data networking consortium. [online] network world (2019).
  2. 2.
  3. 3.
    NFD Developer’s Guide. Tech. rep.
  4. 4.
    Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. In: Hatcliff, J., Zucca, E. (eds.) FMOODS/FORTE -2010. LNCS, vol. 6117, pp. 32–46. Springer, Heidelberg (2010). Scholar
  5. 5.
    Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Sifakis, E.: Verification of an AFDX infrastructure using simulations and probabilities. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 330–344. Springer, Heidelberg (2010). Scholar
  6. 6.
    Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2006, pp. 3–12. IEEE Computer Society, Washington (2006)Google Scholar
  7. 7.
    David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for biological systems. Int. J. Softw. Tools Technol. Transfer 17(3), 351–367 (2015)CrossRefGoogle Scholar
  8. 8.
    Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004). Scholar
  9. 9.
    Jacobson, V., Smetters, D.K., Thornton, J.D., Plass, M.F., Briggs, N.H., Braynard, R.L.: Networking named content (2009).
  10. 10.
    Khoussi, S., et al.: Performance evaluation of a NDN forwarder using statistical model checking. CoRR. (2019)
  11. 11.
    Mediouni, B.L., Nouri, A., Bozga, M., Dellabani, M., Legay, A., Bensalem, S.: \(\cal{S}\)BIP 2.0: statistical model checking stochastic real-time systems. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 536–542. Springer, Cham (2018). Scholar
  12. 12.
    Named data networking project. Tech. rep., USA (October 2010).
  13. 13.
    Nouri, A.: Rigorous system-level modeling and performance evaluation for embedded system design. Ph. D. thesis. Grenoble Alpes University, France (2015)Google Scholar
  14. 14.
    Nouri, A., Bensalem, S., Bozga, M., Delahaye, B., Jegourel, C., Legay, A.: Statistical model checking QoS properties of systems with SBIP. Int. J. Softw. Tools Technol. Transfer (STTT) 17(2), 171–185 (2015)CrossRefGoogle Scholar
  15. 15.
    Nouri, A., Bozga, M., Molnos, A., Legay, A., Bensalem, S.: ASTROLABE: a rigorous approach for system-level performance modeling and analysis. ACM Trans. Embedded Comput. Syst. 15(2), 31:1–31:26 (2016)CrossRefGoogle Scholar
  16. 16.
    Nouri, A., Mediouni, B.L., Bozga, M., Combaz, J., Bensalem, S., Legay, A.: Performance evaluation of stochastic real-time systems with the SBIP framework. Int. J. Crit. Comput.-Based Syst. 8(3–4), 340–370 (2018)CrossRefGoogle Scholar
  17. 17.
    Xylomenos, G., et al.: A survey of information-centric networking research. IEEE Commun. Surv. Tutorials 16(2), 1024–1049 (2014)CrossRefGoogle Scholar
  18. 18.
    Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph. D. thesis, Carnegie Mellon (2005)Google Scholar
  19. 19.
    Zhang, L., et al.: Named data networking. SIGCOMM Comput. Commun. Rev. 44(3), 66–73 (2014)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Siham Khoussi
    • 1
    • 2
  • Ayoub Nouri
    • 1
  • Junxiao Shi
    • 2
  • James Filliben
    • 2
  • Lotfi Benmohamed
    • 2
  • Abdella Battou
    • 2
  • Saddek Bensalem
    • 1
    Email author
  1. 1.Univ. Grenoble Alpes, CNRS, Grenoble Institute of Engineering Univ. Grenoble Alpes, VERIMAGGrenobleFrance
  2. 2.National Institute of Standards and TechnologyGaithersburgUSA

Personalised recommendations