Examinando por Materia "ESPECIFICACIONES"

Mostrando1 - 4 de 4
  • Ponencia en Congreso
    Automated workarounds from Java Program specifications based on SAT solving
    (2017) Uva, Marcelo; Ponzio, Pablo; Regis, Germán; Aguirre, Nazareno; Frías, Marcelo
    "The failures that bugs in software lead to can sometimes be bypassed by the so called workarounds: when a (faulty) routine fails, alternative routines that the system offers can be used in place of the failing one, to circumvent the failure. Previous works have exploited this workarounds notion to automatically recover from runtime failures in some application domains. However, existing approaches that compute workarounds automatically either require the user to manually build an abstract model of the software under consideration, or to provide equivalent sequences of operations from which workarounds are computed, diminishing the automation of workaround-based system recovery. In this paper, we present two techniques that automatically compute workarounds from Java code equipped with formal specifications, avoiding abstract software models and user provided equivalences. These techniques employ SAT solving to compute workarounds on concrete program state characterizations. The first employs SAT solving to compute traditional workarounds, while the second directly exploits SAT solving to circumvent a failing method, building a state that mimics the (correct) behaviour of this failing routine. Our experiments, based on case studies involving implementations of collections and a library for date arithmetic, enable us to show that the techniques can effectively compute workarounds from complex contracts in an important number of cases, in time that makes them feasible to be used for run time repairs."
  • Artículo de Publicación Periódica
    Automated workarounds from Java program specifications based on SAT solving
    (2018-11) Uva, Marcelo; Ponzio, Pablo; Regis, Germán; Aguirre, Nazareno; Frías, Marcelo
    "The failures that bugs in software lead to can sometimes be bypassed by the so-called workarounds: when a (faulty) routine fails, alternative routines that the system offers can be used in place of the failing one, to circumvent the failure. Existing approaches to workaround-based system recovery consider workarounds that are produced from equivalent method sequences, utomatically computed from user-provided abstract models, or directly produced from user-provided equivalent sequences of operations. In this paper, we present two techniques for computing workarounds from Java code equipped with formal specifications, that improve previous approaches in two respects. First, the particular state where the failure originated is actively involved in computing workarounds, thus leading to repairs that are more state specific. Second, our techniques automatically compute workarounds on concrete program state characterizations, avoiding abstract software models and user-provided equivalences. The first technique uses SAT solving to compute a sequence of methods that is equivalent to a failing method on a specific failing state, but which can also be generalized to schemas for workaround reuse. The second technique directly exploits SAT to circumvent a failing method, building a state that mimics the (correct) behaviour of a failing routine, from a specific program state too. We perform an experimental evaluation based on case studies involving implementations of collections and a library for date arithmetic, showing that the techniques can effectively compute workarounds from complex contracts in an important number of cases, in time that makes them feasible to be used for run-time repairs. Our results also show that our state-specific workarounds enable us to produce repairs in many cases where previous workaround-based approaches are inapplicable."
  • Ponencia en Congreso
    EvoSpex: An evolutionary algorithm for learning postconditions (artifact)
    (2021) Molina, Facundo; Ponzio, Pablo; Aguirre, Nazareno; Frías, Marcelo
    "Having the expected behavior of software specified in a formal language can greatly improve the automation of software verification activities, since these need to contrast the intended behavior with the actual software implementation. Unfortunately, software many times lacks such specifications, and thus providing tools and techniques that can assist developers in the construction of software specifications are relevant in software engineering. As an aid in this context, we present EvoSpex, a tool that given a Java method, automatically produces a specification of the method’s current behavior, in the form of postcondition assertions. EvoSpex is based on generating software runs from the implementation (valid runs), making modifications to the runs to build divergent behaviors (invalid runs), and executing a genetic algorithm that tries to evolve a specification to satisfy the valid runs, and leave out the invalid ones. Our tool supports a rich JML-like assertion language, that can capture complex specifications, including sophisticated object structural properties."
  • Artículo de Publicación Periódica
    Improving lazy abstraction for SCR specifications through constraint relaxation
    (2018-03) Degiovanni, Renzo; Ponzio, Pablo; Aguirre, Nazareno; Frías, Marcelo
    "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."