Runtime verification in Erlang by using contracts

Vista sencilla de ítem
dc.contributor.authorFredlund, Lars-Åkees_ES
dc.contributor.authorMariño, Julioes_ES
dc.contributor.authorPérez-Rubio, Sergioes_ES
dc.contributor.authorTamarit Muñoz, Salvadores_ES
dc.contributor.funderComunidad de Madrides_ES
dc.contributor.funderGeneralitat Valencianaes_ES
dc.contributor.funderMinisterio de Economía y Competitividades_ES
dc.date.accessioned2021-01-15T04:31:34Z
dc.date.available2021-01-15T04:31:34Z
dc.date.issued2019es_ES
dc.description.abstract[EN] 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 designby-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.en_EN
dc.description.accrualMethodSes_ES
dc.description.bibliographicCitationFredlund, L.; Mariño, J.; Pérez-Rubio, S.; Tamarit Muñoz, S. (2019). Runtime verification in Erlang by using contracts. Lecture Notes in Computer Science. 11285:56-73. https://doi.org/10.1007/978-3-030-16202-3_4es_ES
dc.description.referencesAntoy, 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_4es_ES
dc.description.referencesArts, 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)es_ES
dc.description.referencesCarlsson, 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)es_ES
dc.description.referencesCassar, 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)es_ES
dc.description.referencesColombo, 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_29es_ES
dc.description.referencesEricsson AB: EDoc (2018). http://erlang.org/doc/apps/edoc/chapter.htmles_ES
dc.description.referencesFredlund, 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)es_ES
dc.description.referencesHanus, 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_19es_ES
dc.description.referencesHerranz, Á., 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_9es_ES
dc.description.referencesJimenez, 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)es_ES
dc.description.referencesLeino, 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_20es_ES
dc.description.referencesLindahl, 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_7es_ES
dc.description.referencesLorenz, D.H., Skotiniotis, T.: Extending design by contract for aspect-oriented programming. CoRR, abs/cs/0501070 (2005)es_ES
dc.description.referencesMeyer, B.: Applying “Design by Contract”. IEEE Comput. 25(10), 40–51 (1992)es_ES
dc.description.referencesPitidis, 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_9es_ES
dc.description.referencesPlociniczak, 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_5es_ES
dc.description.referencesRondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: PLDI 2008, pp. 159–169. ACM (2008)es_ES
dc.description.sponsorshipThis 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 PROMETEOII/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.es_ES
dc.description.upvformatpfin73es_ES
dc.description.upvformatpinicio56es_ES
dc.description.volume11285es_ES
dc.identifier.doi10.1007/978-3-030-16202-3_4es_ES
dc.identifier.issn0302-9743es_ES
dc.identifier.urihttps://riunet.upv.es/handle/10251/159142
dc.languageIngléses_ES
dc.publisherSpringer-Verlages_ES
dc.relation.conferencedateSeptiembre 06-06,2018es_ES
dc.relation.conferencename26th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2018)es_ES
dc.relation.conferenceplaceFrankfurt am Main, Germanyes_ES
dc.relation.ispartofLecture Notes in Computer Sciencees_ES
dc.relation.ispartofFunctional and Constraint Logic Programminges_ES
dc.relation.pasarelaS\403311es_ES
dc.relation.projectIDinfo:eu-repo/grantAgreement/CAM//S2013%2FICE-2731/es_ES
dc.relation.projectIDinfo:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/es_ES
dc.relation.projectIDinfo:eu-repo/grantAgreement/GVA//APOSTD%2F2016%2F036/es_ES
dc.relation.projectIDinfo:eu-repo/grantAgreement/MINECO//TIN2016-76843-C4-1-R/ES/METODOS RIGUROSOS PARA EL INTERNET DEL FUTURO/es_ES
dc.relation.publisherversionhttps://doi.org/10.1007/978-3-030-16202-3_4es_ES
dc.relation.references10.1007/978-3-642-27694-1_4es_ES
dc.relation.references10.1145/1159789.1159792es_ES
dc.relation.references10.1145/1159789.1159791es_ES
dc.relation.references10.1145/3123569.3123570es_ES
dc.relation.references10.1007/978-3-642-29860-8_29es_ES
dc.relation.references10.1007/978-3-319-94460-9_19es_ES
dc.relation.references10.1007/978-3-642-04570-7_9es_ES
dc.relation.references10.1145/1292520.1292523es_ES
dc.relation.references10.1007/978-3-642-17511-4_20es_ES
dc.relation.references10.1007/978-3-540-30477-7_7es_ES
dc.relation.references10.1109/2.161279es_ES
dc.relation.references10.1007/978-3-642-24276-2_9es_ES
dc.relation.references10.1007/978-3-642-13414-2_5es_ES
dc.relation.references10.1145/1375581.1375602es_ES
dc.rightsReserva de todos los derechoses_ES
dc.rights.accessRightsAbiertoes_ES
dc.subjectRuntime verificationes_ES
dc.subjectDesign-by-contractes_ES
dc.subjectProgram instrumentationes_ES
dc.subjectConcurrencyes_ES
dc.subject.classificationLENGUAJES Y SISTEMAS INFORMATICOSes_ES
dc.subject.classificationCIENCIAS DE LA COMPUTACION E INTELIGENCIA ARTIFICIALes_ES
dc.titleRuntime verification in Erlang by using contractses_ES
dc.typeArtículoes_ES
dc.typeComunicación en congresoes_ES
dc.typeCapítulo de libroes_ES
dc.type.versioninfo:eu-repo/semantics/publishedVersiones_ES
dspace.entity.typePublication
upv.uuid99cdfebc-d030-4d89-82aa-57ca8d7e3a1ces_ES

Archivos

Bloque original

Mostrando 1 - 2 de 2
Miniatura
Nombre:
Fredlund;Mariño;Pérez-Rubio - Runtime verification in Erlang by using contracts.pdf
Tamaño:
569.21 KB
Formato:
Adobe Portable Document Format
Descripción:
Versión del Autor.
[object Object] Descargar
Miniatura
Nombre:
RuntimeVerificationInErlang_Version_Editorial.pdf
Tamaño:
1.21 MB
Formato:
Adobe Portable Document Format
Descripción:
Versión editorial
Descargar

Colecciones

Artículos, conferencias, monografías