- -

Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME system

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME system

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: AlpuenteBallisSap ...
Tamaño: 1.125Mb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: MICS2020-editor.pdf
Tamaño: 2.570Mb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Alpuente Frasnedo, María es_ES
dc.contributor.author Ballis, D. es_ES
dc.contributor.author Sapiña-Sanchis, Julia es_ES
dc.date.accessioned 2021-09-04T03:41:08Z
dc.date.available 2021-09-04T03:41:08Z
dc.date.issued 2020-09 es_ES
dc.identifier.issn 1661-8270 es_ES
dc.identifier.uri http://hdl.handle.net/10251/171423
dc.description.abstract [EN] Program specialization is mainly recognized as a powerful technique for optimizing software systems. Nonetheless, it can also be productively employed in other application areas. This paper presents an assertion-guided program specialization methodology for efficiently imposing safety properties on software systems. The program specializer takes as input a set A of logical assertions that specifies the expected system behavior plus a software system that is modeled as a Maude program R that may violate some of the assertions in A. The outcome is a safe refinement R of R in which every system computation is a good run of R, i.e., it satisfies the assertions in A. The specialization technique has been fully automated in the ATAME system and ensures that no good run of R is removed from R, while the number of bad runs is reduced to zero. The efficiency and scalability of our technique is empirically demonstrated by means of a thorough experimental evaluation of the ATAME system, which shows fast specialization times and good performance of the computed specializations, even for large assertion sets. es_ES
dc.description.sponsorship This work has been partially supported by the EU (FEDER) and the Spanish Ministry of Science, Innovation and Universities under grant RTI2018-094403-B-C32, and by Generalitat Valenciana ref. PROMETEO/2019/098 and ref. APOSTD/2019/127. es_ES
dc.language Inglés es_ES
dc.publisher Springer es_ES
dc.relation.ispartof Mathematics in Computer Science es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Safety properties es_ES
dc.subject Assertions es_ES
dc.subject Program transformation es_ES
dc.subject Maude es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME system es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1007/s11786-020-00455-3 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//APOSTD%2F2019%2F127/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEO%2F2019%2F098/ES/DeepTrust: Deep Logic Technology for Software Trustworthiness/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C32/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Alpuente Frasnedo, M.; Ballis, D.; Sapiña-Sanchis, J. (2020). Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME system. Mathematics in Computer Science. 14(3):591-606. https://doi.org/10.1007/s11786-020-00455-3 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion https://doi.org/10.1007/s11786-020-00455-3 es_ES
dc.description.upvformatpinicio 591 es_ES
dc.description.upvformatpfin 606 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 14 es_ES
dc.description.issue 3 es_ES
dc.relation.pasarela S\403081 es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder Agencia Estatal de Investigación es_ES
dc.contributor.funder European Regional Development Fund es_ES
dc.description.references Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Using conditional trace slicing for improving maude programs. Sci. Comput. Program. 80(Part B), 385–415 (2014) es_ES
dc.description.references Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Slicing-based trace analysis of rewriting logic specifications with iJulienne. In: Proceedings of the 22nd European Symposium on Programming (ESOP 2013). LNCS, vol. 7792, pp. 121–124. Springer (2013) es_ES
dc.description.references Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Assertion-based analysis via slicing with ABETS. Theory Pract. Log. Program. 16(5–6), 515–532 (2016) es_ES
dc.description.references Alpuente, M., Ballis, D., Sapiña, J.: Inferring safe Maude programs with ÁTAME. In: Mathematical Software—ICMS 2018—6th International Conference. LNCS, vol. 10931, pp. 1–10. Springer (2018) es_ES
dc.description.references Alpuente, M., Ballis, D., Sapiña, J.: Imposing assertions in Maude via program transformation. MethodsX 6, 2577–2583 (2019) es_ES
dc.description.references Alpuente, M., Ballis, D., Sapiña, J.: Static correction of Maude programs with assertions. J. Syst. Softw. 153, 64–85 (2019) es_ES
dc.description.references Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: Partial evaluation of order-sorted equational programs modulo axioms. In: Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016). LNCS, vol. 10184, pp. 3–20. Springer (2016) es_ES
dc.description.references Clavel, M., Durán, F., Eker, S., Escobar, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude manual (version 3.0). Technical report, SRI International Computer Science Laboratory (2019). http://maude.lcc.uma.es/maude30-manual-html/maude-manual.html. Accessed 24 Jan 2020 es_ES
dc.description.references Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: Proceedings of POPL 2000, pp. 54–66. ACM (2000) es_ES
dc.description.references Danvy, O., Glück, R., Thiemann, P. (eds.): Proceedings of the International Seminar on Partial Evaluation (Dagstuhl 1996). LNCS, vol. 1110. Springer (1996) es_ES
dc.description.references Joiner, R., Reps, T., Jha, S., Dhawan, M., Ganapathy, V.: Efficient runtime-enforcement techniques for policy weaving. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2014), pp. 224–234. ACM (2014) es_ES
dc.description.references Khoo, S.C., Shi, K.: Program adaptation via output-constraint specialization. High. Order Symb. Comput. 17(1), 93–128 (2004) es_ES
dc.description.references Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992) es_ES
dc.description.references Puebla, G., Bueno, F., Hermenegildo, M.V.: Combined static and dynamic assertion-based debugging of constraint logic programs. In: Proceedings of the 9th International Workshop on Logic Programming Synthesis and Transformation (LOPSTR 1999), Selected Papers. LNCS, vol. 1817, pp. 273–292. Springer (2000) es_ES
dc.description.references The Anima Website (2015). http://safe-tools.dsic.upv.es/anima. Accessed 24 Jan 2020 es_ES
dc.description.references Vazou, N., Seidel, E.L., Jhala, R.: LiquidHaskell: experience with refinement types in the real world. In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, pp. 39–51 (2014) es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem