A model driven methodology for the construction of reliable concurrent software

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 tradi- tional 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 defin- ing 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 specifica- tion. 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 lan- guages 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 method- ology, the presented methodology concludes by presenting a property-based testing tech- nique developed using Erlang and Erlang QuickCheck. This phase is composed of two solu- tions 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.