Advertisement

Runtime Verification in Erlang by Using Contracts

  • Lars-Åke Fredlund
  • Julio Mariño
  • Sergio PérezEmail author
  • Salvador Tamarit
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11285)

Abstract

During its lifetime, a program regularly undergoes changes that seek to improve its functionality or efficiency. However, such modifications may also introduce new errors. In this work, we use the design-by-contract approach to allow programmers to formally state, in the code, some of the knowledge and assumptions originally made when the code was first written. Such contracts can then be checked at runtime, to ensure that modifications made to a program did not violate those assumptions. Applying these principles we have designed a runtime verification system for the Erlang language, permitting to specify as annotations the contracts needed for both sequential and concurrent code. As a second contribution we extend the commonly used Erlang gen_server behaviour (a design pattern) permitting to specify declaratively when a server is ready to service a client request. The ideas presented in this paper have been implemented in a tool named EDBC. Its source code is available at github.com as an open-source and free project.

Keywords

Runtime verification Design-By-Contract Program instrumentation Concurrency 

References

  1. 1.
    Antoy, S., Hanus, M.: Contracts and specifications for functional logic programming. In: Russo, C., Zhou, N.-F. (eds.) PADL 2012. LNCS, vol. 7149, pp. 33–47. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-27694-1_4CrossRefGoogle Scholar
  2. 2.
    Arts, T., Hughes, J., Johansson, J., Wiger, U.T.: Testing telecoms software with quviq QuickCheck. In: Proceedings of the 2006 ACM SIGPLAN Workshop on Erlang, pp. 2–10. ACM (2006)Google Scholar
  3. 3.
    Carlsson, R., Rémond, M.: EUnit: a lightweight unit testing framework for Erlang. In: Feeley, M., Trinder, P.W. (eds.) Proceedings of the 2006 ACM SIGPLAN Workshop on Erlang, p. 1. ACM (2006)Google Scholar
  4. 4.
    Cassar, I., Francalanza, A., Aceto, L., Ingólfsdóttir, A.: eAOP: an aspect oriented programming framework for Erlang. In: Chechina, N., Fritchie, S.L. (eds.) Proceedings of the 16th ACM SIGPLAN International Workshop on Erlang, pp. 20–30. ACM (2017)Google Scholar
  5. 5.
    Colombo, C., Francalanza, A., Gatt, R.: Elarva: a monitoring tool for Erlang. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 370–374. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-29860-8_29CrossRefGoogle Scholar
  6. 6.
  7. 7.
    Fredlund, L., Mariño, J., Alborodo, R.N., Herranz, Á.: A testing-based approach to ensure the safety of shared resource concurrent systems. Proc. Inst. Mech. Eng. Part O: J. Risk Reliab. 230(5), 457–472 (2016)Google Scholar
  8. 8.
    Hanus, M.: Combining static and dynamic contract checking for curry. In: Fioravanti, F., Gallagher, J.P. (eds.) LOPSTR 2017. LNCS, vol. 10855, pp. 323–340. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-94460-9_19CrossRefzbMATHGoogle Scholar
  9. 9.
    Herranz, Á., Mariño, J., Carro, M., Moreno Navarro, J.J.: Modeling concurrent systems with shared resources. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 102–116. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04570-7_9CrossRefGoogle Scholar
  10. 10.
    Jimenez, M., Lindahl, T., Sagonas, K.: A language for specifying type contracts in Erlang and its interaction with success typings. In: Thompson, S.J., Fredlund, L. (eds.) Proceedings of the 2007 ACM SIGPLAN Workshop on Erlang, Freiburg, Germany, 5 October 2007, pp. 11–17. ACM (2007)Google Scholar
  11. 11.
    Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17511-4_20CrossRefzbMATHGoogle Scholar
  12. 12.
    Lindahl, T., Sagonas, K.: Detecting software defects in telecom applications through lightweight static analysis: a war story. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 91–106. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30477-7_7CrossRefGoogle Scholar
  13. 13.
    Lorenz, D.H., Skotiniotis, T.: Extending design by contract for aspect-oriented programming. CoRR, abs/cs/0501070 (2005)Google Scholar
  14. 14.
    Meyer, B.: Applying “Design by Contract”. IEEE Comput. 25(10), 40–51 (1992)CrossRefGoogle Scholar
  15. 15.
    Pitidis, M., Sagonas, K.: Purity in Erlang. In: Hage, J., Morazán, M.T. (eds.) IFL 2010. LNCS, vol. 6647, pp. 137–152. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-24276-2_9CrossRefGoogle Scholar
  16. 16.
    Plociniczak, H., Eisenbach, S.: JErlang: Erlang with joins. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 61–75. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-13414-2_5CrossRefGoogle Scholar
  17. 17.
    Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: PLDI 2008, pp. 159–169. ACM (2008)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Lars-Åke Fredlund
    • 1
  • Julio Mariño
    • 1
  • Sergio Pérez
    • 2
    Email author
  • Salvador Tamarit
    • 2
  1. 1.Babel GroupUniversidad Politécnica de MadridMadridSpain
  2. 2.Departament de Sistemes Informàtics i ComputacióUniversitat Politècnica de ValènciaValenciaSpain

Personalised recommendations