artículo de publicación periódica.page.titleprefix
Improving lazy abstraction for SCR specifications through constraint relaxation

Simple item page
dc.contributor.authorDegiovanni, Renzo
dc.contributor.authorPonzio, Pablo
dc.contributor.authorAguirre, Nazareno
dc.contributor.authorFrías, Marcelo
dc.date.accessioned2020-06-26T20:09:54Z
dc.date.available2020-06-26T20:09:54Z
dc.date.issued2018-03
dc.description.abstract"Formal requirements specifications, eg, software cost reduction (SCR) specifications, are challenging to analyse using automated techniques such as model checking. Since such specifications are meant to capture requirements, they tend to refer to real-world magnitudes often characterized through variables over large domains. At the same time, they feature a high degree of nondeterminism, as opposed to other analysis contexts such as (sequential) program verification. This makes model checking of SCR specifications difficult even for symbolic approaches. Moreover, automated abstraction refinement techniques such as counterexample guided abstraction refinement fail in many cases in this context, since the concrete state space is typically large, and reaching specific states of interest may require complex executions involving many different states, causing these approaches to perform many abstraction refinements, and making them ineffective in practice. In this paper, an approach to tackle the above situation, through a 2-stage abstraction, is presented. The specification is first relaxed, by disregarding the constraints imposed in the specification by physical laws or by the environment, before being fed to a counterexample guided abstraction refinement procedure, tailored to SCR. By relaxing the original specification, shorter spurious counterexamples are produced, favouring the abstraction refinement through the introduction of fewer abstraction predicates. Then, when a counterexample is concretizable with respect to the relaxed (concrete) specification but it is spurious with respect to the original specification, an efficient though incomplete refinement step is applied to the constraints, to cause the removal of the spurious case. This approach is experimentally assessed, comparing it with related techniques in the verification of properties and in automated test case generation, using various SCR specifications drawn from the literature as case studies. The experiments show that this new approach runs faster and scales better to larger, more complex specifications than related techniques."en
dc.identifier.issn0960-0833
dc.identifier.urihttp://ri.itba.edu.ar/handle/123456789/2228
dc.language.isoenen
dc.relationinfo:eu-repo/semantics/altIdentifier/doi/10.1002/stvr.1657
dc.relationinfo:eu-repo/grantAgreement/ANPCyT/PICT/2012-1298/AR. Ciudad Autónoma de Buenos Aires
dc.relationinfo:eu-repo/grantAgreement/ANPCyT/PICT/2013-2624/AR. Ciudad Autónoma de Buenos Aires
dc.relationinfo:eu-repo/grantAgreement/ANPCyT/PICT/2015-2341/AR. Ciudad Autónoma de Buenos Aires
dc.relationinfo:eu-repo/grantAgreement/ANPCyT/PICT/2015-2088/AR. Ciudad Autónoma de Buenos Aires
dc.relationinfo:eu-repo/grantAgreement/QNRF/NPRP/4-1109-1-174/QA. Doha
dc.subjectESPECIFICACIONESes
dc.subjectINGENIERIA DE SOFTWAREes
dc.subjectVERIFICACION DE SOFTWAREes
dc.titleImproving lazy abstraction for SCR specifications through constraint relaxationen
dc.typeArtículos de Publicaciones Periódicases
dc.typeinfo:eu-repo/semantics/acceptedVersion
dspace.entity.typeArtículo de Publicación Periódica
itba.description.filiationFil: Degiovanni, Renzo. Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas, Físico-Químicas y Naturales; Argentina.
itba.description.filiationFil: Degiovanni, Renzo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina.
itba.description.filiationFil: Ponzio, Pablo. Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas, Físico-Químicas y Naturales; Argentina.
itba.description.filiationFil: Ponzio, Pablo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina.
itba.description.filiationFil: Aguirre, Nazareno. Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas, Físico-Químicas y Naturales; Argentina.
itba.description.filiationFil: Aguirre, Nazareno. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina.
itba.description.filiationFil: Frías, Marcelo. Instituto Tecnológico de Buenos Aires; Argentina.
itba.description.filiationFil: Frías, Marcelo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina.

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
1Degiovanni_2018_ING_INFORMATICA.pdf
Size:
2.54 MB
Format:
Adobe Portable Document Format
Description:
Articulo_Degiovanni
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.6 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

Artículos de publicaciones periódicas