TRIADE aims at using formal models with structuring programmatic constructs as means to translate programs and descriptions written in formalisms widely used in Embedded System and SoC design, and provide a seamless flow of increasingly time-defined and time-accurate models, so as to progressively obtain the final mapped implementation through provably correct steps from the early description elements.

General information

Starting date. march 2009.

Project coordinators: Robert de Simone and Jean-Pierre Talpin

Presentation. The design of Real-Time Embedded (RT/E) Systems is currently a field of encounter between numerous methods and techniques developed independently, for specific purposes and often in different aims. A current grand challenge is to combine them into a global coherent design flow, each at its appropriate modeling level. The overall objective is to best map complex applications onto heterogeneous architectures, the former comprising latent (logical) concurrency while the latter offer (physical) intrinsic parallelism with contrived communication structures.

The TRIADE Collaborative Research Initiatives (in french, Action de Recherche Collaborative - ARC) of INRIA aims to tackle these issues using formal model developments and by using techniques pertaining to Concurrency Theory, Scheduling Theory, Compilation and Optimization Theories, Model Driven Engineering and Electronic System Level design altogether. In some cases, the models are currently put forth in the approach, in others they are somehow buried under some algorithmic treatments. Exhibiting them and making their relations explicit is the focus of the project.

The models adopted by TRIADE require precise formal semantics and, more specifically, precise mathematical modeling for logic, temporal and timing aspects. This is required so that the subsequent transformations, abstractions and refinements are provably sound and semantic preserving. This should be opposed to the mainstream model-driven approach, where (certainly useful) higher-level models are simply put next to a lower-level implementation counter-parts, as if proximity alone would make them behave "the same".

In this prominent, informal approach the models are sometimes explicitly concurrent descriptions which correspond to (lower-level) sequential simulation code (as often in UML or Simulink). On the opposite, they are also sometimes seemingly sequential simulation descriptions, that are in turn synthesized into (lower-level) parallel hardware (as in TLM SystemC or High-Performance Computing nested loop code). TRIADE would like to consider both kinds of transformations, as well as the general case where models of computations are refined one into another. Its approach requires a number of formal restrictions on the type of models dealt with. This, again, can be opposed to the larger setting where general-purpose programming languages are naively used, but where often hidden synthesizability side conditions crawl in incidentally at hidden places. The belief in TRIADE is that the clarity of assumptions (which often match mandatory requirements in the RT/E domain anyway) is a prerequisite of sound model-based design approach.

TRIADE shall build on techniques and theories that have been for a long-time developed inside INRIA or in the neighboring French research community, and in fact can often be traced back to the original C3 (Cooperation, Communication, Concurrency) nation-wide initiative of the mid-1980s. Typical examples are: Models of Computations and Communications (MoCCs) such as Process Algebras, Timed Event Graphs and Synchronous Reactive Languages; model-based scheduling techniques (with periodic steady regimes); nested loop parallelizing and optimization; distributed real-time scheduling; optimized compilation onto micro-architectures with instruction- and task-level parallelism, model-based and platform-based design in the field of embedded systems; high-performance and grid computing... (list not exhaustive).

Precise links between formalisms on their time aspects, for instance by using formal semantics concepts of modules systems and type theory, is in our view a necessary condition for a true component-based approach of design, where the same object can be considered at various levels of realization, with some amount of confidence that the contract promised at some external level will be satisfied (in some well-defined sense) by the implementation. Clear understanding of time is a prerequisite for interoperability in co-simulation. By contrast, current attempts amount all too often to exercising jointly various simulators in a step mode, without real concern for established formal coherency of the whole (just plausibility of results).

Of course, it has to be realized that in "real-life" these approximate practices are already providing many helps in early system evaluation, improving on most current practices. But, given that precise comparative semantic links exist at places, we want to push further the limits of true model-based design for RT/E systems wherever feasible. The good news is that, but dealing with formal models and semantics, one gets very often rich automatic optimization techniques (which apply under well-established conditions).