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.
This work has been partially supported by MINECO/AEI/FEDER (EU) under grant TIN2016-76843-C4-1-R, by the Comunidad de Madrid under grant S2013/ICE-2731 (N-Greens Software), and by the Generalitat Valenciana under grant PROMETEO-II/2015/013 (SmartLogic). Salvador Tamarit was partially supported by the Conselleria de Educación, Investigación, Cultura y Deporte de la Generalitat Valenciana under grant APOSTD/2016/036.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
For example, process links help structure fault detection and fault recovery in complex applications.
- 2.
As an implementation decision, we have chosen to use Erlang macros to represent all contracts. The reason is that similar tools like EUnit also use macros for assert definitions.
- 3.
Note that decreasing-argument contracts only guarantee termination if the sequence is strictly decreasing and well founded, i.e. values cannot go below a certain limit.
- 4.
The from of the request has the same form as in the handle_call/3 callback, i.e., a tuple {Pid,Tag}, where Pid is the process identifier of the client issuing the request, and Tag is a unique tag.
- 5.
- 6.
- 7.
References
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_4
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)
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)
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)
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_29
Ericsson AB: EDoc (2018). http://erlang.org/doc/apps/edoc/chapter.html
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)
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_19
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_9
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)
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_20
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_7
Lorenz, D.H., Skotiniotis, T.: Extending design by contract for aspect-oriented programming. CoRR, abs/cs/0501070 (2005)
Meyer, B.: Applying “Design by Contract”. IEEE Comput. 25(10), 40–51 (1992)
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_9
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_5
Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: PLDI 2008, pp. 159–169. ACM (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Fredlund, LÅ., Mariño, J., Pérez, S., Tamarit, S. (2019). Runtime Verification in Erlang by Using Contracts. In: Silva, J. (eds) Functional and Constraint Logic Programming. WFLP 2018. Lecture Notes in Computer Science(), vol 11285. Springer, Cham. https://doi.org/10.1007/978-3-030-16202-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-16202-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-16201-6
Online ISBN: 978-3-030-16202-3
eBook Packages: Computer ScienceComputer Science (R0)