SAT-Based Combinatorial Testing

Abstract

En aquesta tesi ens centrem en el problema de Combinatorial Testing mitjançant l'aplicació de la tecnologia de Satisfactibilitat. L'objectiu de CT és proveir d'un conjunt de proves que permeti capturar la majoria dels errors en un Sistema Sota Prova (SUT). En particular, presentem diversos algorismes per a generar Covering Arrays Mixtes amb Restriccions (MCACs). En primer lloc, mostrem com aplicar la tecnologia de la Màxima Satisfactibilitat per a generar MCACs òptims i subòptims. En segon lloc, mostrem com computar MCACs amb strengths altes de manera efectiva (considerant strengths t>4) mitjançant l'aplicació de nous algorismes incomplets i solucions paral·leles. En tercer lloc, presentem el disseny i la implementació d'un nou generador d'instàncies per a Combinatorial Testing que utilitza instàncies del problema de la Satisfactibilitat per a generar SUTs artificials. Addicionalment, hem sigut capaços d'extraure diverses receptes sobre quin algorisme de MCAC aplicar a un SUT determinat. Tots els algorismes dissenyats durant aquesta tesi s'han implementat dins del paquet CTLog. Finalment, descrivim les nostres contribucions al framework de Python OptiLog, pensat per al desenvolupament d'aplicacions basades en la tecnologia SAT, el qual s'ha utilitzat per tal de crear CTLog.

En esta tesis abarcamos el problema de Combinatorial Testing (CT) mediante la aplicación de la tecnología de Satisfactibilidad. El objetivo de CT es proveer un conjunto de pruebas que permita capturar la mayoría de los errores en un Sistema Bajo Prueba (SUT). En particular, presentamos varios algoritmos para generar Covering Arrays Mixtos y con Restricciones (MCACs). En primer lugar, mostramos como aplicar la tecnología de la Máxima Satisfactibilidad para generar MCACs óptimos y subóptimos. En segundo lugar, mostramos como computar MCACs con strengths altas de manera efectiva (considerando strengths t>4) mediante la aplicación de nuevos algoritmos incompletos y soluciones paralelas. En tercer lugar, presentamos el diseño y la implementación de un nuevo generador de instancias para Combinatorial Testing que utiliza instancias del problema de la Satisfactibilidad para generar SUTs artificiales. Adicionalmente, hemos sido capaces de extraer distintas recetas sobre qué algoritmo de MCAC aplicar a un SUT determinado. Todos los algoritmos diseñados durante esta tesis han sido implementados en el paquete CTLog. Finalmente, describimos nuestras contribuciones en el framework de Python OptiLog, pensado para el desarrollo de aplicaciones basadas en la tecnología SAT, el cual ha sido utilizado para crear CTLog.

In this thesis, we address the Combinatorial Testing (CT) problem through the application of Satisfiability technology. The goal of CT is to provide a test suite that is used to capture most of the errors or bugs in a System Under Test (SUT). In particular, we present several algorithms for the generation of Mixed Covering Arrays with Constraints (MCAC). First, we show how to apply Maximum Satisfiability technology to generate optimal and suboptimal MCACs. Second, we show how to effectively compute high-strength MCACs (considering strengths t>4) by applying new incomplete algorithms and parallel solutions. Third, we design and implement a new benchmark generator for Combinatorial Testing that uses instances from the Satisfiability problem to generate new crafted SUTs. We also provide insights and recipes on which MCAC algorithm should be used for a particular SUT. All the algorithms designed during this thesis have been implemented into the CTLog package. Finally, we describe our contributions to the OptiLog Python framework for the development of SAT-based applications that we used to create CTLog.