Examinando por Materia "VERIFICACION DE SOFTWARE"

Mostrando1 - 10 de 10
  • Ponencia en Congreso
    An analysis of the suitability of test-based patch acceptance criteria
    (2017-07) Zemín, Luciano; Gutiérrez Brida, Simón; Godio, Ariel; Cornejo, César; Degiovanni, Renzo; Regis, Germán; Aguirre, Nazareno; Frías, Marcelo
    "Program repair techniques attempt to fix programs by looking for patches within a search space of fix candidates. These techniques require a specification of the program to be repaired, used as an acceptance criterion for fix candidates, that often also plays an important role in guiding some search processes. Most tools use tests as specifications, which constitutes a risk, since the incompleteness of tests as specifications may lead one to obtain spurious repairs, that pass all tests but are in fact incorrect. This problem has been identified by various researchers, raising concerns about the validity of program fixes. More thorough studies have been proposed using different sets of tests for fix validation, and resorting to manual inspection, showing that while tools reduce their program fixing rate, they are still able to repair a significant number of cases. In this paper, we perform a different analysis of the suitability of tests as acceptance criteria for automated program fixes, by checking patches produced by automated repair tools using a bug-finding tool, as opposed to previous works that used tests or manual inspections. We develop a number of experiments in which faulty programs from a known benchmark are fed to the program repair tools GenProg, Angelix, AutoFix and Nopol, using test suites of varying quality and extension, including those accompanying the benchmark. We then check the produced patches against formal specifications using a bug-finding tool. Our results show that, in general, automated program repair tools are significantly more likely to accept a spurious program fix than producing an actual one, in the studied scenarios. "
  • Trabajo final de especialización
    Aseguramiento de la calidad en la construcción de sistemas basados en el conocimiento: un enfoque práctico
    (2003) Diez, Eduardo; García Martínez, Ramón; Britos, Paola Verónica
    "La función de aseguramiento de la calidad del software (SQA) se debe basar en un planificado y sistemático diseño de acciones y métodos, requeridos para garantizar la calidad del mismo. En el presente trabajo, se presenta un diseño de acciones y métodos que constituyen un enfoque práctico para el desempeño de la función de SQA en una organización, adaptado especialmente a la metodología IDEAL para el desarrollo de sistemas basados en el conocimiento. Este enfoque no pretende ser exclusivo y en ningún caso limita o inhibe la aplicación de otras acciones, métodos o modelos, sino que podrá ser su complemento, adaptándolo convenientemente. El enfoque o modelo de aseguramiento de la calidad del software que tiene las siguientes características: El modelo de aseguramiento de calidad de software sugerido es una interfaz a una metodología, IDEAL en este caso, de desarrollo de software. El modelo que aquí se presenta no es una metodología en sí misma, sino que debe acoplarse a una metodología de desarrollo para poder implementarse. Esta interfaz está compuesta por módulos independientes, donde cada uno de ellos se asocia a ciertos procesos de la metodología IDEAL."
  • Ponencia en Congreso
    Automatically identifying sufficient object builders from Module APIs
    (2019) Ponzio, Pablo; Bengolea, Valeria; Politano, Mariano; Aguirre, Nazareno; Frías, Marcelo
    "Various approaches to software analysis (e.g. test input generation, software model checking) require engineers to (manually) identify a subset of a module’s methods in order to drive the analysis. Given a module to be analyzed, engineers typically select a subset of its methods to be considered as object builders to define a so-called driver, that will be used to automatically build objects for analysis, e.g., combining them non-deterministically, randomly, etc. This requires a careful inspection of the module and its API, since both the relative exhaustiveness of the analysis (leaving important methods out may systematically avoid generating different objects), as well as its efficiency (the different bounded combinations of methods grows exponentially as the number of methods increases), are affected by the selection. We propose an approach for automatically selecting a set of builders from a module’s API, based on an evolutionary algorithm that favors sets of methods whose combinations lead to producing larger sets of objects. The algorithm also takes into account other characteristics of these sets of methods, trying to prioritize the selection of methods with less and simpler parameters. As the implementation of this evolutionary mechanism requires in principle handling and comparing large sets of objects, and this grows very quickly both in terms of space and running times, we employ an abstraction of sets of objects, called field extensions, that involves using the field values of the objects in the set instead of the actual objects, and enables us to effectively implement our mechanism. An experimental assessment on a benchmark of stateful classes shows that our approach can automatically identify sets of builders that are sufficient (can be used to create any instance of the module) and minimal (do not contain superfluous methods), in a reasonable time."
  • Ponencia en Congreso
    DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour
    (2017-09) Regis, Germán; Cornejo, César; Gutiérrez Brida, Simón; Politano, Mariano; Raverta, Fernando; Ponzio, Pablo; Aguirre, Nazareno; Galeotti, Juan Pablo; Frías, Marcelo
    "We describe DynAlloy Analyzer, a tool that extends Alloy Analyzer with support for dynamic elements in Alloy models. The tool builds upon Alloy Analyzer in a way that makes it fully compatible with Alloy models, and extends their syntax with a particular idiom, inspired in dynamic logic, for the description of dynamic behaviours, understood as sequences of states over standard Alloy models, in terms of programs. The syntax is broad enough to accommodate abstract dynamic behaviours, e.g., using nondeterministic choice and finite unbounded iteration, as well as more concrete ones, using standard sequential programming constructions. The analysis of DynAlloy models resorts to the analysis of Alloy models, through an optimized translation that often makes the analysis more efficient than that of typical ad-hoc constructions to capture dynamism in Alloy."
  • Artículo de Publicación Periódica
    An evolutionary approach to translating operational specifications into declarative specifications
    (2019-07) Molina, Facundo; Cornejo, César; Degiovanni, Renzo; Regis, Germán; Castro, Pablo; Aguirre, Nazareno; Frías, Marcelo
    "Various tools for program analysis, including run-time assertion checkers and static analyzers such as verification and test generation tools, require formal specifications of the programs being analyzed. Moreover, many of these tools and techniques require such specifications to be written in a particular style, or follow certain patterns, in order to obtain an acceptable performance from the corresponding analyses. Thus, having a formal specification sometimes is not enough for using a particular technique, since such specification may not be provided in the right formalism. In this paper, we deal with this problem in the increasingly common case of having an operational specification, while for analysis reasons requiring a declarative specification. We propose an evolutionary approach to translate an operational specification written in a sequential programming language, into a declarative specification, in relational logic. We perform experiments on a benchmark of data structure implementations, for which operational invariants are available, and show that our evolutionary computation based approach to translating specifications achieves very good precision in this context, and produces declarative specifications that are more amenable to analyses that demand specifications in this style. This is assessed in two contexts: bounded verification of data structure invariant preservation, and instance enumeration using symbolic execution aided by tight bounds."
  • 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."
  • Proyecto final de Grado
    Generación automática de casos de test para criterios de código avanzados
    (2014) Homovc, Federico; Pintos, Esteban; De Santi, Matías; Frías, Marcelo
    "El testing de software es una de las tecnologías más utilizadas en el análisis y valida-ción de sistemas. El mismo consiste en ejecutar el sistema desarrollado sobre inputs particulares, y verificar que los outputs producidos se correspondan con lo esperado. La generación automática de inputs para testeo de software es un área de investigación y desarrollo muy activa, con conferencias de primer nivel que dedican sesiones a la misma (por ejemplo ICST –International Conference on Software Testing-, ICSE -International Conference on Software Engineering-, ASE –Automated Software Engineering-, lo hacen). En el marco del testeo de software existen diversos criterios de coberturas de código que sirven para determinar la calidad de un conjunto de inputs de testeo. Por ejemplo, la cobertura de sentencias requiere que cada sentencia del programa sea ejecutada al menos una vez por alg ́un test. La herramienta FAJITA permite al usuario elegir un criterio de cobertura y llevarlo a cabo. Actualmente FAJITA permite utilizar los criterios de cobertura de sentencias, de condiciones y de objetivos, pero existen otros que a ́un no son soportados. El objetivo de este proyecto es entonces extender el portfolio de criterios de cobertura ofrecidos por dicha herramienta."
  • 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."
  • Proyecto final de Grado
    Relif: a relation algebra specification tool
    (2019-12-19) Lynch, Marcelo María; Frías, Marcelo
    "Relation algebras are algebras arising from the study of binary relations. They form a part of the eld of algebraic logic, and have applications in proof theory, modal logic, and computer science. An interesting problem in relation algebras is the representation problem, which is to give a canonical representation of a given relation algebra, in the form of binary relations. This problem doesn't have a solution for all algebras. This paper presents Relif, a specication tool that allows the user to explore relation algebras satisfying a set of constraints dened by the user, and provides a way of looking for representations."
  • Proyecto final de Grado
    Verificación utilizando Dynamite de la corrección del modelo Chord
    (2019-08-12) Dantur, Juan Pablo; Ocamica, Santiago; Frías, Marcelo; Moscato, Mariano
    "La herramienta Dynamite permite traducir modelos formales realizados en el lenguaje de modelado Alloy en teorías del demostrador semiautomático PVS, pero no fue probado con modelos tan complejos como un modelo completo del protocolo Chord. El objetivo inicial de este trabajo fue demostrar la correctitud del protocolo Chord utilizando Dynamite. Durante el desarrollo del Proyecto Final nos encontramos con limitaciones relacionadas a la traducción de Alloy a PVS por parte de Dynamite. Por este motivo, el objetivo del trabajo pasó a ser el de probar Dynamite con el modelo de Chord mencionado anteriormente y de esta forma evaluar la aplicabilidad de Dynamite para este objetivo. Se pudo contribuir al avance de Dynamite a través del reporte de problemas relacionados a la traducción del modelo de Alloy de Chord. También quedaron demostrados con Dynamite todos los lemas sobre los espacios de identificadores y dos de los cinco teoremas principales sobre la correctitud de Chord dado que su invariante se cumple."