This dissertation introduces Pikse, a novel methodology for more effective and efficient checking of code conformance to specifications using parallel and incremental techniques, describes a prototype implementation that embodies the methodology, and presents experiments that demonstrate its efficacy. Pikse has at its foundation a well-studied approach -- systematic constraint-driven analysis -- that has two common forms: (1) constraint-based testing -- where logical constraints that define desired inputs and expected program behavior are used for test input generation and correctness checking, say to perform black-box testing; and (2) symbolic execution -- where a systematic exploration of (bounded) program paths using symbolic input values is used to check properties of program behavior, say to perform white-box testing. Our insight at the heart of Pikse is that for certain path-based analyses, (1) the state of a run of the analysis can be encoded compactly, which provides a basis for parallel techniques that have low communication overhead; and (2) iterations performed by the analysis have commonalities, which provides the basis for incremental techniques that re-use results of computations common to successive iterations. We embody our insight into a suite of parallel and incremental techniques that enable more effective and efficient constraint-driven analysis. Moreover, our techniques work in tandem, for example, for combined black-box constraint-based input generation with white-box symbolic execution. We present a series of experiments to evaluate our techniques. Experimental results show Pikse enables significant speedups over previous state-of-the-art. / text

Tesis por compendio / [ES] Erlang es un lenguaje de programación funcional con concurrencia mediante paso de mensajes basado en el modelo de actores. Éstas y otras características lo hacen especialmente adecuado para aplicaciones distribuidas en tiempo real acrítico. En los últimos años, la popularidad de Erlang ha aumentado debido a la demanda de servicios concurrentes. No obstante, desarrollar sistemas Erlang libres de errores es un reto considerable. A pesar de que Erlang evita muchos problemas por diseño (por ejemplo, puntos muertos), algunos otros problemas pueden aparecer. En este contexto, las técnicas de testing y depuración basadas en métodos formales pueden ser útiles para detectar, localizar y arreglar errores de programación en Erlang. En esta tesis proponemos varios métodos para testing y depuración en Erlang. En particular, estos métodos están basados en modelos semánticos para concolic testing, pruebas basadas en propiedades, depuración reversible con consistencia causal y repetición reversible con consistencia causal de programas Erlang. Además, probamos formalmente las principales propiedades de nuestras propuestas y diseñamos herramientas de código abierto que implementan estos métodos. / [CA] Erlang és un llenguatge de programació funcional amb concurrència mitjançant pas de missatges basat en el model d'actors. Estes i altres característiques el fan especialment adequat per a aplicacions distribuïdes en temps real acrític. En els últims anys, la popularitat d'Erlang ha augmentat degut a la demanda de servicis concurrents. No obstant, desenvolupar sistemes Erlang lliures d'errors és un repte considerable. Encara que Erlang evita molts problemes per disseny (per exemple, punts morts), alguns altres problemes poden aparéixer. En este context, les tècniques de testing y depuració basades en mètodes formals poden ser útils per a detectar, localitzar y arreglar errors de programació en Erlang. En esta tesis proposem diversos mètodes per a testing i depuració en Erlang. En particular, estos mètodes estan basats en models semàntics per a concolic testing, testing basat en propietats, depuració reversible amb consistència causal i repetició reversible amb consistència causal de programes Erlang. A més, provem formalment les principals propietats de les nostres propostes i dissenyem ferramentes de codi obert que implementen estos mètodes. / [EN] Erlang is a message-passing concurrent, functional programming language based on the actor model. These and other features make it especially appropriate for distributed, soft real-time applications. In the recent years, Erlang's popularity has increased due to the demand for concurrent services. However, developing error-free systems in Erlang is quite a challenge. Although Erlang avoids many problems by design (e.g., deadlocks), some other problems may appear. Here, testing and debugging techniques based on formal methods may be helpful to detect, locate and fix programming errors in Erlang. In this thesis we propose several methods for testing and debugging in Erlang. In particular, these methods are based on semantics models for concolic testing, property-based testing, causal-consistent reversible debugging and causal-consistent replay debugging of Erlang programs. We formally prove the main properties of our proposals and design open-source tools that implement these methods. / Palacios Corella, A. (2020). Formal Methods for Constraint-Based Testing and Reversible Debugging in Erlang [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/139076 / Compendio

Le test à base de modèles des systèmes réactifs est le processus de vérifier si un système sous test (SUT) est conforme à sa spécification. Il consiste à gérer à la fois la génération des données de test et le calcul de verdicts en utilisant des modèles. Nous spécifions le comportement des systèmes réactifs à l'aide des systèmes de transitions symboliques temporisées à entrée-sortie (TIOSTS). Quand les TIOSTSs sont utilisés pour tester des systèmes avec une interface centralisée, l'utilisateur peut ordonner complètement les événements (i.e., les entrées envoyées au système et les sorties produites). Les interactions entre le testeur et le SUT consistent en des séquences d'entrées et de sortie nommées traces, pouvant être séparées par des durées dans le cadre du test temporisé, pour former ce que l'on appelle des traces temporisées. Les systèmes distribués sont des collections de composants locaux communiquant entre eux et interagissant avec leur environnement via des interfaces physiquement distribuées. Différents événements survenant à ces différentes interfaces ne peuvent plus être ordonnés. Cette thèse concerne le test de conformité des systèmes distribués où un testeur est placé à chaque interface localisée et peut observer ce qui se passe à cette interface. Nous supposons qu'il n'y a pas d’horloge commune mais seulement des horloges locales pour chaque interface. La sémantique de tels systèmes est définie comme des tuples de traces temporisées. Nous considérons une approche du test dans le contexte de la relation de conformité distribuée dtioco. La conformité globale peut être testée dans une architecture de test en utilisant des testeurs locaux sans communication entre eux. Nous proposons un algorithme pour vérifier la communication pour un tuple de traces temporisées en formulant le problème de message-passing en un problème de satisfaction de contraintes (CSP). Nous avons mis en œuvre le calcul des verdicts de test en orchestrant à la fois les algorithmes du test centralisé off-line de chacun des composants et la vérification des communications par le biais d'un solveur de contraintes. Nous avons validé notre approche sur un cas étude de taille significative. / Model-based testing of reactive systems is the process of checking if a System Under Test (SUT) conforms to its model. It consists of handling both test data generation and verdict computation by using models. We specify the behaviour of reactive systems using Timed Input Output Symbolic Transition Systems (TIOSTS) that are timed automata enriched with symbolic mechanisms to handle data. When TIOSTSs are used to test systems with a centralized interface, the user may completely order events occurring at this interface (i.e., inputs sent to the system and outputs produced from it). Interactions between the tester and the SUT are sequences of inputs and outputs named traces, separated by delays in the timed framework, to form so-called timed traces. Distributed systems are collections of communicating local components which interact with their environment at physically distributed interfaces. Interacting with such a distributed system requires exchanging values with it by means of several interfaces in the same testing process. Different events occurring at different interfaces cannot be ordered any more. This thesis focuses on conformance testing for distributed systems where a separate tester is placed at each localized interface and may only observe what happens at this interface. We assume that there is no global clock but only local clocks for each localized interface. The semantics of such systems can be seen as tuples of timed traces. We consider a framework for distributed testing from TIOSTS along with corresponding test hypotheses and a distributed conformance relation called dtioco. Global conformance can be tested in a distributed testing architecture using only local testers without any communication between them. We propose an algorithm to check communication policy for a tuple of timed traces by formulating the verification of message passing in terms of Constraint Satisfaction Problem (CSP). Hence, we were able to implement the computation of test verdicts by orchestrating both localised off-line testing algorithms and the verification of constraints defined by message passing that can be supported by a constraint solver. Lastly, we validated our approach on a real case study of a telecommunications distributed system.