PhD Thesis
A MARTE-Based Reactive Model for Data-Parallel Intensive Processing:
Transformation Toward the Synchronous Model
Jean-Luc Dekeyser, Professor, USTL
Éric Rutten, Research scientist, INRIA
Abdoulaye Gamatie, Research scientist, CNRS
The context of this dissertation is the assistance of embedded system design, in particular Systems-on-Chip (SoC). The complexity of such systems, and their strong interaction with their environments, cause the problems of sophisticated design (to avoid the late error detections, the average cost of the diagnostics and repairing, also the time-to-market), and of verification and certification for safety critical system (need to be verified before their issues). In consequence, there is a strong need for methods and tools to assist safe design of these systems (take the form of methodologies and of component-based models, of high-level specification languages, of transformation and compiling tools, of analysis and verification, of synthesis and code generation).
More precisely, The work presented in this dissertation is carried out in the Gaspard2 framework, which is dedicated to SoC design for data-parallel intensive processing applications (DIAs). Examples of such applications are found in multimedia processing and signal processing. On the one hand, safe design of DIAs is considered to be important due to the need of Quality of Service, safety criticality, etc., in these applications. However, the complexity of current embedded systems makes it difficult to meet this requirement. On the other hand, high-level safe control, is highly demanded in order to ensure the correctness and strengthen the flexibility and adaptivity of DIAs.
As an answer to the mentioned issue, we propose to take advantage of synchronous languages to assist safe DIA design. Synchronous languages enable the specification of unambiguous system behavior for reactive systems. In addition, large number of formal validation tools built around these languages contribute to ensure the correctness design of reactive embedded systems, particularly certain safety critical systems, such as avionic, automobile and power plant.
First, a synchronous modeling bridges the gap between Gaspard2 and synchronous languages. This modeling contributes to the transformation of Gaspard2 specifications into programs in synchronous languages. The latter, together with their associated tools, enable high-level validation of Gaspard2 specifications. An intermediate model, i.e., the synchronous equational model, is the result of the synchronous modeling. On one hand, this model preserves the properties of original Gaspard2 specifications, such as multidimensional array data structure, data dependency, single assignment, task parallelism, data parallelism, etc. The preserved properties contributes to guarantee that verifications carried out on this model or the executable code generated from this model is also valid for the Gaspard2 model. On the other hand, it only keeps common aspects of synchronous dataflow languages (Lustre, Signal and Lucid synchrone) in order that it is simple and generic, hence the complexity and particularity of target languages is avoided in this model. It enables to generate these three languages from only one model.
Secondly, a reactive extension to a previous control proposition in Gaspard2, is also addressed. This extension is based on mode automata and contributes to conferring safe and verifiable features onto the previous proposition. These features includes composition operators that contribute to the specification of complex systems, and formal semantics that enable the utilization of formal validation and synthesis techniques, such as model checking and discrete controller synthesis. In addition, as Gaspard2 is not associated with an execution model, the difference between the Gaspard2 specification model and synchronous execution model is also discussed, which helps to map the former to the latter.
Finally, a Model-Driven Engineering (MDE) approach is adopted in order to implement and validate our proposition, as well as benefit from the advantages of MDE to address system complexity and productivity issues. Synchronous modeling, MARTE-based (the UML profile for Modeling and Analysis of Real-Time and Embedded system) control modeling, and model transformations, including code generation, are dealt with in the implementation.