Tesis:
A Model Driven Methodology for the Construction of Reliable Concurrent Software
- Autor: ALBORODO, Raúl Nestor Neri
- Título: A Model Driven Methodology for the Construction of Reliable Concurrent Software
- Fecha: 2019
- Materia: Sin materia definida
- Escuela: E.T.S DE INGENIEROS INFORMÁTICOS
- Departamentos: LENGUAJES Y SISTEMAS INFORMATICOS E INGENIERIA DE SOFTWARE
- Acceso electrónico: http://oa.upm.es/57809/
- Director/a 1º: MARIÑO CARBALLO, Julio
- Resumen: The software development process now requires a working knowledge of parallel and distributed programming. The requirement for a piece of software to work properly over some shared resources is a universal must nowadays. Users want instantaneous and reliable results. In many situations the user wants the software to satisfy a number of requests at the same time. Software must be designed to take advantage of computers that have multiple processors and must be designed to run correctly and effectively. However, such systems are hard to program, and ensuring quality by means of traditional testing techniques is often useless as errors may not show up easily and reproducing them is hard. Even though testing is one of the most widely used approach to partial system validation, the introduction of concurrency makes exhaustive testing extremely costly, and impossible in some scenarios. Due to that, industry is trying to shift to formal verification techniques. This thesis proposes a model-driven methodology (guided by Design by Contracts (DbC) technique) for designing and verifying safety-critical concurrent system implementations using shared resources. This methodology is divided into three phases: analysis and design, code generation and testing and verification. The whole process starts from a mathematical specification of the shared resource defining the precise behaviour of the shared resource using the well- know DbC technique. Then, it is automatically translated into TLA in order to check that some concurrency properties hold, for instance, being free of deadlocks, and that there is no inconsistency in the specification. If no error was detected, the next step is the generation of traceable code by following a set of templates for implementing the shared resource in several languages (like Java, Erlang, Ada,etc.). Once the model has been validated, a certified code in a variety of programming languages can be generated. This is achieved by dividing the system into client process (light code) and the shared resource (heavy code) where all the concurrency specific constructs are placed. This method is language independent, non-intrusive for the development process, and improves the portability of the resulting system. Even though the methodology is language-independent, this thesis is mainly focused on the problem of generating concurrent Java code from high-level interactive models (Erlang implementations are also included in this book showing that models can be easily translated even when the language is functional). Using an extension of the Java Modeling Language for specifying shared resources as Java interfaces, the process describes how to translate those formal models into shared memory (using a priority monitors library) or message passing (using the JCSP library) implementations. The code generation process can be fully automatic or semi automatic, but in both cases the obtained code is traceable. Both, the validation of the JML model and part of the code generation process, are constructed over the existing and well-known JML tool-set. During this phase, a set of well defined proof obligations are added as runtime assertion checking code (RAC), to each of the patterns to ensure that the generated code is correct. After that and because the programmer still retains the power of coding or modifying parts of the code for the resource, an instrumentation process followed by the verification of the instrumented code is presented using KeY verifier. Finally, in the case that the code of the shared resource is not obtained using this methodology, the presented methodology concludes by presenting a property-based testing technique developed using Erlang and Erlang QuickCheck. This phase is composed of two solutions that are iterative and inclusive: (i) testing an implemented system in order to check if it faithfully conforms to the resource specification on which it is based; (ii) testing a network of shared resources, i.e. a set of shared resources that have to be assembled together to perform a task and communicate with each other following a (well-formed) protocol. ----------RESUMEN---------- El proceso de desarrollo de software requiere ahora un conocimiento práctico de la programación paralela y distribuida. El requisito de que una pieza de software funcione correctamente en conjunto con algunos recursos compartidos es una necesidad universal hoy en día. Los usuarios quieren resultados instantáneos y fiables. En muchas situaciones, el usuario desea que el software procese varias peticiones al mismo tiempo, con lo cual debe estar diseñado para aprovechar las ventajas de las computadoras que tienen múltiples procesadores y debe estar diseñado para funcionar correcta y eficazmente. Sin embargo, estos sistemas son difíciles de programar, y a menudo resulta inútil garantizar la calidad mediante técnicas de pruebas tradicionales, ya que los errores pueden no aparecer fácilmente y su reproducción es muy complicada. Aunque metodologías de testing son uno de los enfoques más utilizados para la validación parcial del sistema, la introducción de la concurrencia hace que las pruebas exhaustivas sean extremadamente costosas e imposibles en la mayoría de los escenarios. Debido a ello, la industria está tratando de mudarse a las técnicas de verificación formal. Esta tesis propone una metodología basada en modelos (guiada por la técnica Design by Contracts (DbC)) para diseñar y verificar implementaciones seguras de sistemas concurrentes críticos que utilicen recursos compartidos. Esta metodología se divide en tres fases: análisis y diseño, generación de código y testing y verificación. Todo el proceso parte de una especificación matemática del recurso compartido definiendo el comportamiento preciso del recurso compartido utilizando la conocida técnica DbC. A continuación, se traduce automáticamente a TLA para comprobar que algunas propiedades de concurrencia se cumplen, como por ejemplo, que esté libres de bloqueos, y que no hay inconsistencias en la especificación en si. Si no se detecta ningún error, el siguiente paso es la generación de código rastreable utilizando un conjunto de plantillas para implementar el recurso compartido en varios lenguajes (como Java, Erlang, Ada, etc.). Esto se logra dividiendo el sistema en proceso cliente (código ligero) y recurso compartido (código pesado) donde se colocan todas las construcciones específicas para el manejo de la concurrencia. Este método es independiente del lenguaje, no intrusivo para el proceso de desarrollo y mejora la portabilidad del sistema resultante. Aunque la metodología es independiente del lenguaje, esta tesis se centra principalmente en el problema de generar código Java concurrente a partir de modelos interactivos de alto nivel (las implementaciones de Erlang también se incluyen en este libro, demostrando que los modelos pueden ser fácilmente traducidos incluso cuando el lenguaje es funcional). Usando una extensión del Java Modeling Language para especificar recursos compartidos como interfaces Java, este processo describe cómo traducir esos modelos formales en implementaciones de memoria compartida (usando una biblioteca de monitores de prioridad) o de paso de mensajes (usando la biblioteca JCSP). La fase de generación de código puede ser totalmente automática o semiautomática, pero en ambos casos el código obtenido es trazable. Tanto la validación del modelo JML como parte del proceso de generación de código, se construyen sobre el conjunto de herramientas JML existentes y conocidas. Durante esta fase, un conjunto de obligaciones de prueba bien definidas se añaden como código de comprobación (en forma de aserciones en tiempo de ejecución) a cada uno de los patrones para asegurar que el código generado es correcto. Luego, y debido a que el programador aún conserva el poder de implementar o modificar partes del código para el recurso, se presenta un proceso de instrumentación para su posterior verificación del código instrumentado utilizando KeY Verifier. Finalmente, en caso de tener código de un recurso compartido que no ha sido generado mediante este enfoque, la metodología presentada concluye con la presentación de una técnica de testing basada en propiedades desarrollada utilizando Erlang y Erlang QuickCheck. Esta fase se compone de dos soluciones que son iterativas e inclusivas: (i) probar que un sistema para comprobar se ajusta fielmente a la especificación y (ii) probar que una red de recursos compartidos, es decir, un conjunto de recursos compartidos que deben ensamblados para realizar una tarea y comunicarse entre sí siguiendo un protocolo (bien definido).