Verification of Concurrent Systems: optimality, Scalability and Applicability
Miguel Isabel Márquez · Dialnet (Universidad de la Rioja) · 2020
Tanto el testing como la verificacion de sistemas concurrentes requieren explorar todos los posibles entrelazados no deterministas que la ejecucion concurrente puede tener, ya que cualquiera de estos entrelazados podria revelar un comportamiento erroneo del sistema. Esto introduce una explosion combinatoria en el numero 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 tecnicas novedosas para el testing y la verificacion de programas concurrentes que permitan reducir esta explosion combinatoria. La reduccion basada en ordenes parciales (POR) es una teoria general que ayuda a mitigar esta explosion mediante la identificacion formal de clases de equivalencia de exploraciones redundantes. Tales clases de equivalencia son conocidas como trazas de Mazurkiewicz, y la teoria 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 tecnicas de reduccion basada en ordenes parciales. El pilar fundamental de la teor??a POR es la nocion de independencia, que es usada para decidir si cada par de pasos de ejecucion 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 dinamico basado en POR (DPOR), que fue un avance fundamental en este area. Actualmente, DPOR es considerada una de las tecnicas mas escalables para el testing y la verificacion de sistemas concurrentes. Optimal-DPOR (ODPOR) es una extension que garantiza optimalidad, explorando solamente una ejecucion por cada clase de equivalencia. Ambos algoritmos estan basados en una relacion de (in)dependencia incondicional que determina el orden parcial de cada par de transiciones. La nocion de independencia condicional fue introducida en 1992 en el contexto de POR, donde fue demostrado que solamente una nocion de independencia condicional uniforme puede ser utilizada correctamente. El primer algoritmo que ha usado nociones de independencia condicional dentro del algoritmo DPOR clasico es conocido como Context-Sensitive DPOR (DPORcs). Recientemente, Optimal DPOR with Observers (ODPORob) ha introducido la nocion de observabilidad, segun la cual, la dependencia entre dos pasos de ejecucion esta 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 nocion de independencia condicional dentro de los algoritmos DPOR, usando restricciones de independencia (ICs), que garanticen la conmutatividad entre pasos de ejecucion; iii. realizar una evaluacion experimental que permita medir las tecnicas propuestas; y iv. aplicar estas tecnicas a un escenario realista. Los analisis estaticos aportan informacion util acerca de los programas analizados y puede ser usado para mejorar el comportamiento del testing. Para ello, se han propuesto dos retos mas: v. combinar el analisis estatico y el testing para la deteccion efectiva de deadlocks, y vi. extender este marco de trabajo al contexto de la ejecucion simbolica. En esta tesis hemos propuesto soluciones para todos los retos descritos y hemos llevado a cabo una evaluacion experimental para cada uno de ellos. Esta evaluacion experimental permite afirmar que el uso de nociones de independencia condicional dentro de los algoritmos DPOR mejora los resultados de las tecnicas actuales. Finalmente, el uso del analisis estatico para guiar el proceso del testing ayuda a mitigar todavia mas el problema de la explosion de estados.