Modelado y verificación del protocolo de exclusión mutua con tiempo real Fischer usando Maude

Abstract

[ES] En el siguiente trabajo modelamos el protocolo de exclusión mutua con tiempo real Fischer como un módulo de sistema mediante el lenguaje de especificación y verificación Maude. Hacemos uso del alcance de la generación de estados y del model checker de Maude para verificar las propiedades de exclusión mutua, deadlock freedom y vivacidad. Para conseguir este objetivo, en la primera parte enseñamos los conceptos básicos de dos lenguajes de especificación y verificación, Maude y CafeOBJ. Para apoyar la explicación, presentamos un ejemplo de especificación en Maude de un cruce con dos semáforos con vehículos, y hacemos un ejemplo de verificación de una propiedad de seguridad en él. Luego hacemos un estudio del recorrido del protocolo Fischer, desde sus orígenes hasta la versión propuesta más reciente, para comprender las implicaciones que tiene sobre el uso del tiempo. A continuación, analizamos una versión propuesta en el lenguaje CafeOBJ. Estudiamos la construcción del modelo, así como las asunciones temporales que se hacen sobre él. Además, mostramos la verificación de la propiedad de exclusión mutua realizada mediante proof score method, un método de verificación propio de CafeOBJ. Luego definimos un modelo, en el lenguaje de especificación Maude, para el protocolo de exclusión mutua en tiempo real Fischer. Sobre este modelo comentamos las decisiones de diseño del tiempo y sus límites, tanto globales como específicos. Con el modelo definido, empleamos la herramienta de model checking disponible en el lenguaje Maude, para definir las propiedades de exclusión mutua, deadlock freedom y vivacidad, como fórmulas en la lógica conocida como linear temporal logic. Hacemos uso de las fórmulas sobre dos estados que definimos en el model checker, y conseguimos verificar la propiedad de exclusión mutua para nuestro modelo. Para las otras dos propiedades explicamos las razones por las cuales no han podido ser verificadas y proponemos una solución para la propiedad deadlock freedom.

[EN] In the following work we model Fischer¿s real-time mutual exclusion protocol as a system module using the Maude specification and verification language. We make use of the scope of the generation of states and Maude¿s model checker to verify the properties of mutual exclusion, deadlock freedom and starvation freedom. To achieve this goal, in the first part we teach the basics of two specification and verification languages, Maude and CafeOBJ. To support the explanation, we present an example of a specification in Maude of a crossing with two traffic lights with vehicles, and we do an example of verification of a safety property on it. We then do a study of the journey of the Fischer protocol, from its origins to the most recent proposed version, to understand the implications it has on the use of time. Next, we analyze a version proposed in the CafeOBJ language. We study the construction of the model, as well as the temporal assumptions that are made about it. In addition, we show the verification of the mutual exclusion property carried out using the proof score method, a verification method of CafeOBJ. We then define a model, in the Maude specification language, for the Fischer real-time mutual exclusion protocol. On this model we discuss the design decisions of time and its limits, both global and specific. With the model defined, we use the model checking tool available in the Maude language, to define the properties of mutual exclusion, deadlock freedom and vivacity, as formulas in the logic known as linear temporal logic. We make use of the two-state formulas that we define in the model checker, and we manage to verify the mutual exclusion property for our model. For the other two properties we explain the reasons why they could not be verified and propose a solution for deadlock freedom.