Improving lazy abstraction for SCR specifications through constraint relaxation

"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 throu...

Descripción completa

Detalles Bibliográficos
Autores principales: Degiovanni, Renzo, Ponzio, Pablo, Aguirre, Nazareno, Frías, Marcelo
Formato: Artículos de Publicaciones Periódicas acceptedVersion
Lenguaje:Inglés
Publicado: 2020
Materias:
ESPECIFICACIONES
INGENIERIA DE SOFTWARE
VERIFICACION DE SOFTWARE
Acceso en línea:http://ri.itba.edu.ar/handle/123456789/2228
Aporte de:
Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA) de Instituto Tecnológico de Buenos Aires (ITBA)
id I32-R138-123456789-2228
record_format dspace
spelling I32-R138-123456789-22282022-12-07T13:05:52Z Improving lazy abstraction for SCR specifications through constraint relaxation Degiovanni, Renzo Ponzio, Pablo Aguirre, Nazareno Frías, Marcelo ESPECIFICACIONES INGENIERIA DE SOFTWARE VERIFICACION DE SOFTWARE "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." 2020-06-26T20:09:54Z 2020-06-26T20:09:54Z 2018-03 Artículos de Publicaciones Periódicas info:eu-repo/semantics/acceptedVersion 0960-0833 http://ri.itba.edu.ar/handle/123456789/2228 en info:eu-repo/semantics/altIdentifier/doi/10.1002/stvr.1657 info:eu-repo/grantAgreement/ANPCyT/PICT/2012-1298/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ANPCyT/PICT/2013-2624/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ANPCyT/PICT/2015-2341/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/ANPCyT/PICT/2015-2088/AR. Ciudad Autónoma de Buenos Aires info:eu-repo/grantAgreement/QNRF/NPRP/4-1109-1-174/QA. Doha application/pdf
institution Instituto Tecnológico de Buenos Aires (ITBA)
institution_str I-32
repository_str R-138
collection Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA)
language Inglés
topic ESPECIFICACIONES
INGENIERIA DE SOFTWARE
VERIFICACION DE SOFTWARE
spellingShingle ESPECIFICACIONES
INGENIERIA DE SOFTWARE
VERIFICACION DE SOFTWARE
Degiovanni, Renzo
Ponzio, Pablo
Aguirre, Nazareno
Frías, Marcelo
Improving lazy abstraction for SCR specifications through constraint relaxation
topic_facet ESPECIFICACIONES
INGENIERIA DE SOFTWARE
VERIFICACION DE SOFTWARE
description "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."
format Artículos de Publicaciones Periódicas
acceptedVersion
author Degiovanni, Renzo
Ponzio, Pablo
Aguirre, Nazareno
Frías, Marcelo
author_facet Degiovanni, Renzo
Ponzio, Pablo
Aguirre, Nazareno
Frías, Marcelo
author_sort Degiovanni, Renzo
title Improving lazy abstraction for SCR specifications through constraint relaxation
title_short Improving lazy abstraction for SCR specifications through constraint relaxation
title_full Improving lazy abstraction for SCR specifications through constraint relaxation
title_fullStr Improving lazy abstraction for SCR specifications through constraint relaxation
title_full_unstemmed Improving lazy abstraction for SCR specifications through constraint relaxation
title_sort improving lazy abstraction for scr specifications through constraint relaxation
publishDate 2020
url http://ri.itba.edu.ar/handle/123456789/2228
work_keys_str_mv AT degiovannirenzo improvinglazyabstractionforscrspecificationsthroughconstraintrelaxation
AT ponziopablo improvinglazyabstractionforscrspecificationsthroughconstraintrelaxation
AT aguirrenazareno improvinglazyabstractionforscrspecificationsthroughconstraintrelaxation
AT friasmarcelo improvinglazyabstractionforscrspecificationsthroughconstraintrelaxation
_version_ 1765661100745949184

Ejemplares similares