|
Descripción
|
|
|---|---|
| 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. | |
|
Internacional
|
Si |
|
ISBN
|
|
|
Tipo de Tesis
|
Doctoral |
|
Calificación
|
Sobresaliente |
|
Fecha
|
17/12/2019 |