Contributions to Formal Communication Elimination for System Models with Explicit Parallelism

Abstract

Els mètodes de verificació formal s'estan usant cada vegada més en la indústria per establir la correctessa i trobar els errors en models de sistemes; per exemple la descripció de hardware, protocols, programes distribuïts, etc. En particular, els verificadors de models ho fan automàticament per sistemes d'estats finits, per-o estan limitats degut al problema de l'explosió d'estats; i la verificació formal interactiva, l'àrea d'aquesta tesi, es necessita.<br/><br/>L'enfocament de la verificació automàtica treballa sobre el sistema de transicions del model, el qual defineix la seva semàntica. Aquest sistema de transicions té sovint molts estats, i sempre una mida gran comparada amb la mida del model del sistema, el qual és sempre infinit. Aquestes consideracions suggereixen un enfocament de verificació estàtica com els d'aquesta tesi, evitant els sistemes de transicions, treballant directament sobre el model del sistema, en principi, la complexitat computacional hauria de ser menor. L'enfocament estàtic d'aquest treball es fa sobre models de sistemes expressats en notació imperativa amb paral·lelisme explícit, sentències de comunicacions síncrones i variables d'emmagatzematge locals.<br/><br/>Els raonaments d'equivalència són molt empleats per números, matrius i altres camps. Tanmateix, per programes imperatius amb paral·lelisme, comunicacions i variables, encara que potencialment sigui un mètode de verificació molt intuïtiu, no han estat massa explorats. La seqüencialització formal via l'eliminació de comunicacions internes, l'àrea d'aquesta tesi, és una demostració basada en el raonament estàtic d'equivalències que, donat que disminueix la magnitud del vector d'estats, pot complementar altres mètodes de demostració. Es basa en l'aplicació d'un conjunt de lleis , apropiades per tal propòsit, com reduccions de reescriptura del model del sistema. Aquestes depenen de la noció d'equivalència i de les suposicions de justícia.<br/><br/>Aquesta tesi contribueix a la quasi inexplorada àrea de l'eliminació de comunicacions formal i seqüencialització de models de sistema. Les lleis estan definides sobre una equivalència feble: equivalència d'interfície. L'eliminació de comunicacions est-a limitada a models sense seleccions, per exemple models en els quals les comunicacions internes no estan dins de l'àmbit de sentències de selecció. Aplicacions interessants existeixen dins d'aquest marc. Les lleis són vàlides només per justícia feble o sense justícia. Aquesta ha estat desenvolupada seguint la semàntica proposada per Manna i Pnueli per a sistemes reactius [MP91, MP95]. S'han formulat les condicions d'aplicabilitat per les lleis de la pròpia eliminació de comunicacions. A més a més, es proposa un procediment de construcció de demostracions per l'eliminació de comunicacions, el qual intenta aplicar automàticament les lleis de la eliminació. També s'ha dissenyat un conjunt de procediments de transformació, els quals garanteixen que la transformació equivalent sempre correspon a l'aplicació d'una seqüència de lleis. Degut a que la construcció de les demostracions és impracticable, normalment impossible, sense l'ajuda d'una eina, s'ha desenvolupat un demostrador interactiu per la construcció semiautomàtica de la seqüencialització de models de sistemes i demostracions d'eliminació. Tant els procediments de transformació com els de l'eliminació de comunicacions estan integrats en l'eina. Amb l'ajuda del demostrador s'ha construït la demostració de seqüencialització d'un model, no trivial, de processador pipeline. Per aquest exemple s'ha assolit una reducció, respecte del model original, de la cota superior del nombre d'estats de 2&#8722;672.<br/><br/>Malgrat l'enorme quantitat d'esforç dedicat a l'àrea, abans i durant la tesi, encara queda molt treball per a que l'eliminació de comunicacions i la seqüencialització sigui realment un mètode pràctic. No obstant els resultats d'aquesta tesi han establert els fonaments i han donat l'estímul necessari per continuar l'esforç.

Los métodos de verificación formal se están usando cada vez más en la industria para establecer la corrección y encontrar los errores en modelos de sistemas; por ejemplo, la descripción de hardware, protocolos, programas distribuidos, etc. En particular, los verificadores de modelos lo hacen automáticamente para sistemas de estados finitos, pero están limitados debido al problema de la explosión de estados; y la verificación formal interactiva, el área de esta tesis, es necesaria.<br/><br/>El enfoque de la verificación automática trabaja sobre el sistema de transiciones del modelo, el cual define su semántica. Este sistema de transiciones tiene a menudo muchos estados, y siempre un tamaño grande comparado con el tamaño del modelo del sistema, el cual es siempre infinito. Estas consideraciones sugieren un enfoque de verificación estática como los de esta tesis, evitando los sistemas de transiciones, trabajando directamente sobre el modelo del sistema, en principio, la complejidad computacional tendría que ser menor. El enfoque estático de este trabajo se lleva a cabo sobre modelos de sistemas expresados en notación imperativa con paralelismo explícito, sentencias de comunicaciones síncronas y variables de almacenamiento locales.<br/><br/>Los razonamientos de equivalencia son muy empleados para números, matrices y otros campos. Sin embargo, para programas imperativos con paralelismo, comunicaciones y variables, aún teniendo la potencialidad de ser un método de verificación muy intuitivo, no han sido muy explorados. La secuencialización formal vía la eliminación de comunicaciones internas, el área de esta tesis, es una demostración basada en el razonamiento estático de equivalencias que, ya que disminuye la magnitud del vector de estados, puede complementar otros métodos de demostración. Se basa en la aplicación de un conjunto de leyes, apropiadas para tal propósito, como reducciones de reescritura del modelo del sistema. Éstas dependen de la noción de equivalencia y de las suposiciones de justicia.<br/><br/>Esta tesis contribuye a la casi inexplorada área de la eliminación de comunicaciones formal y secuencialización de modelos de sistema. Las leyes están definidas sobre una equivalencia débil: equivalencia de interfaz. La eliminación de comunicaciones está limitada a modelos sin selecciones, por ejemplo modelos en los cuales las comunicaciones internas no están dentro del ámbito de sentencias de selección. Aplicaciones interesantes existen dentro de este marco. Las leyes son válidas sólo para justicia débil o sin justicia. Ésta ha sido desarrollada siguiendo la semántica propuesta por Manna y Pnueli para sistemas reactivos [MP91, MP95]. Se han formulado las condiciones de aplicabilidad para las leyes de la propia eliminación de comunicaciones. Además, se propone un procedimiento de construcción de demostraciones para la eliminación de comunicaciones, el cual intenta aplicar automáticamente las leyes de la eliminación. También se ha diseñado un conjunto de procedimientos de transformación, los cuales garantizan que la transformación equivalente siempre corresponde a la aplicación de una secuencia de leyes. Debido a que la construcción de las demostraciones es impracticable, normalmente imposible, sin la ayuda de una herramienta, se ha desarrollado un demostrador interactivo para la construcción semiautomática de la secuencialización de modelos de sistemas y demostraciones de eliminación. Tanto los procedimientos de transformación como los de la eliminación de comunicaciones están integrados en la herramienta. Con la ayuda del demostrador se ha construido la demostración de secuencialización de un modelo, no trivial, de procesador pipeline. Para este ejemplo se ha logrado una reducción, respecto del modelo original, de la cota superior del número de estados de 2&#8722;672.<br/><br/>A pesar de la enorme cantidad de esfuerzo dedicado al área, antes y durante esta tesis, todavía queda mucho trabajo para que la eliminación de comunicaciones y la secuencialización sea realmente un método práctico. Sin embargo los resultados de esta tesis han establecido los cimientos y han dado el estímulo necesario para continuar el esfuerzo.

Formal verification methods are increasingly being used in industry to establish the correctness of, and to find the flaws in, system models; for instance, descriptions of hardware, protocols, distributed programs, etc. In particular, model checking does that automatically for finite-state systems, but it is limited in scope due to the state explosion problem; and interactive formal verification, the broad area of this thesis, is needed.<br/><br/>Automatic verification approaches work on the transition system of the model, which defines its semantics. This transition system has often infinitely many states, and always a large size compared to the size of the system model, which is always finite. These considerations suggest that static verification approaches such as those of this thesis, avoiding the transition system, working directly on the system model would have less computational complexity, in principle. The static approach of this work is carried out on system models expressed in imperative notations with explicit parallelism and synchronous communication statements, and with local storage variables.<br/><br/>Equivalence reasoning is heavily used for numbers, matrices, and other fields. However, for imperative programs with parallelism, communications, and variables, although having the potentiality of being a very intuitive verification method, it has not been much explored. Formal sequentialization via internal communication elimination, the area of this thesis, is a static equivalence reasoning proof that, since it decreases the size of the state vector, could complement other proof methods. It is based on the application of a set of laws, suitable for that purpose, as rewriting reductions to a system model. These proofs need both proper communication elimination laws and auxiliary basic laws. These depend on the notion of equivalence and on the fairness assumptions.<br/><br/>This thesis contributes to the almost unexplored area of formal communication elimination and system model sequentialization. The laws are defined over a weak equivalence: interface equivalence. Communication elimination is confined to selection-free models, i.e. models none of whose inner communications are within the scope of selection statements. Interesting applications already exist within this framework. The laws are valid only with weak fairness or no fairness. It has been developed following the same semantics as Manna and Pnueli for reactive systems [MP91, MP95]. Applicability conditions for the proper communication elimination laws are derived. In addition, a communication elimination proof construction procedure, which attempts to apply the elimination laws automatically is proposed. A set of transformation procedures, guaranteeing that the equivalence transformation always corresponds to the application of a sequence of laws have been designed as well. Since the construction of elimination proofs is impractical, even impossible, without a tool, an interactive prover for semi-automatic construction of system model sequentialization and elimination proofs has been developed. Both transformation and communication elimination procedures are integrated within the tool. As a non-trivial example, a sequentialization proof of a pipelined processor model, has been constructed with the help of the prover. A<br/>reduction, with respect to the original model, of 2&#8722;672 on the upper bound on the number of states has been achieved in this example.<br/><br/>In spite of the huge amount of effort already devoted to the area, before and during this thesis, much work still needs to be done until communication elimination and sequentialization become a practical method. Nevertheless the results of this thesis have established its foundations and given the necessary encouragement for continuing the effort.