Model-Driven Engineering and Formal Validation of High-Performance Embedded Systems

Abstract

The study presented in this paper concerns the safe design of
high-performance embedded systems, specifically dedicated to intensive
data-parallel processing as found, for instance, in modern multimedia
applications or radar/sonar signal processing. Among the important
requirements of such systems are the efficient execution, reliability
and quality of service. Unfortunately, the complexity of modern
embedded systems makes it difficult to meet all these requirements.

As an answer to this issue, this paper proposes a combination of two
models of computation (MoCs) within a framework, called Gaspard, in
order to deal with the design and validation of high-performance
embedded systems. On the one hand, the repetitive MoC offers a
powerful expression of the parallelism available in both system
functionality and architecture. On the other hand, the synchronous MoC
serves as a formal model on which a trustworthy verification can be
applied. Here, the high-level models specified with the repetitive MoC
are translated into an equational model in the synchronous MoC so as
to be able to formally analyze different properties of the modeled
systems. As an example, a clock synchronizability analysis is
illustrated on a multimedia system in order to guarantee a correct
interaction between its components. For the implementation and
validation of our proposition, a Model-Driven Engineering (MDE)
approach is adopted. MDE is well-suited to deal with design complexity
and productivity issues. In our case, the OMG standard MARTE profile
is used to model embedded systems. Then, automatic transformations are
applied to these models to produce the corresponding synchronous
programs for analysis.