Verification of Concurrent Systemsoptimality, Scalability and Applicability

Resumen

Tanto el testing como la verificación de sistemas concurrentes requieren explorar todos los posibles entrelazados no deterministas que la ejecución concurrente puede tener, ya que cualquiera de estos entrelazados podría revelar un comportamiento erróneo del sistema. Esto introduce una explosión combinatoria en el número de estados del programa que deben ser considerados, lo que lleva a un problema computacionalmente intratable. El objetivo de esta tesis es el desarrollo de técnicas novedosas para el testing y la verificación de programas concurrentes que permitan reducir esta explosión combinatoria. La reducción basada en órdenes parciales (POR) es una teoría general que ayuda a mitigar esta explosión mediante la identificación formal de clases de equivalencia de exploraciones redundantes. Tales clases de equivalencia son conocidas como trazas de Mazurkiewicz, y la teoría POR garantiza que es suficiente explorar un entrelazado por cada clase de equivalencia. Uno de los objetivos principales de esta tesis es el desarrollo de técnicas de reducción basada en órdenes parciales. El pilar fundamental de la teor¿¿a POR es la noción de independencia, que es usada para decidir si cada par de pasos de ejecución p y t son dependientes y, como consecuencia, las ejecuciones p.t y t.p deben ser exploradas. En 2005, Flanagan y Godefroid propusieron un algoritmo dinámico basado en POR (DPOR), que fue un avance fundamental en este área. Actualmente, DPOR es considerada una de las técnicas más escalables para el testing y la verificación de sistemas concurrentes. Optimal-DPOR (ODPOR) es una extensión que garantiza optimalidad, explorando solamente una ejecución por cada clase de equivalencia. Ambos algoritmos están basados en una relación de (in)dependencia incondicional que determina el orden parcial de cada par de transiciones. La noción de independencia condicional fue introducida en 1992 en el contexto de POR, donde fue demostrado que solamente una noción de independencia condicional uniforme puede ser utilizada correctamente. El primer algoritmo que ha usado nociones de independencia condicional dentro del algoritmo DPOR clásico es conocido como Context-Sensitive DPOR (DPORcs). Recientemente, Optimal DPOR with Observers (ODPORob) ha introducido la noción de observabilidad, según la cual, la dependencia entre dos pasos de ejecución está condicionada a la existencia de futuros observadores de tales pasos. Uno de los logros principales de esta tesis es ser capaces de beneficiarse de nociones de independencia condicional. Este logro puede separarse en los siguientes retos: i. combinar y aprovechar las nociones de independencia presentadas en DPORcs y ODPORob y estudiar sus sinergias para obtener mayores reducciones; ii. explotar la propiedad de uniformidad que permite usar la noción de independencia condicional dentro de los algoritmos DPOR, usando restricciones de independencia (ICs), que garanticen la conmutatividad entre pasos de ejecución; iii. realizar una evaluación experimental que permita medir las técnicas propuestas; y iv. aplicar estas técnicas a un escenario realista. Los análisis estáticos aportan información útil acerca de los programas analizados y puede ser usado para mejorar el comportamiento del testing. Para ello, se han propuesto dos retos más: v. combinar el análisis estático y el testing para la detección efectiva de deadlocks, y vi. extender este marco de trabajo al contexto de la ejecución simbólica. En esta tesis hemos propuesto soluciones para todos los retos descritos y hemos llevado a cabo una evaluación experimental para cada uno de ellos. Esta evaluación experimental permite afirmar que el uso de nociones de independencia condicional dentro de los algoritmos DPOR mejora los resultados de las técnicas actuales. Finalmente, el uso del análisis estático para guiar el proceso del testing ayuda a mitigar todavía más el problema de la explosión de estados.