Verimag

Models for the Implementation and the Virtual Prototyping of Embedded Systems

Formal study and definition of system-level models, models for non-functional properties, executable models, faithfulness problems, ...

The Synchrone Group has been studying various kinds of embedded systems models for more than 20 years. A model has several usages. It can either be further refined into some implementation, or be used to validate the functional properties of a system specification, and/or to evaluate the performances of a system before it is actually built. We call virtual prototyping all the approaches in which an executable and system-wide model of a computer system is built and run for various observations. In recent years, the group has applied such an approach to the various levels of abstraction that are used to model embedded control systems (see Embedded Software Implementation), systems-on-a-chip (see VERIMAG + STMicroelectronics common projects [2002...[) and sensor networks. On the other hand, working on abstract models is the key to the understanding of complex computer systems, and helps finding correct-by-construction implementation methods.

We also work on several analysis methods, for functional or non-functional properties. In the latter case, we look for a compromise between fully detailed computational models (which are difficult to analyze), and very abstract analytical models (whose faithfulness can be seriously questioned). Finally, abstract models also serve in developing algorithms; since S. Devismes joined the group in September 2008, some work has been devoted to distributed systems problems.

A system-wide model may include:

  • A simplified model of the physical environment of the computer system (useful for embedded control systems)
  • A model of the execution platform (the hardware, the OS or middleware)
  • A model of the embedded software (that may be extracted automatically from programming languages like C, or obtained as a result of the compilation process from a language like Lustre).

The rest of this text describes several approaches for the definition of formal models. Of course this is not independent of the actual uses of models for the implementation and validation of embedded systems. See also Embedded Software Implementation for more details.


Contact | Site Map | Site created with SPIP 2.1.26 + AHUNTSIC [CC License]

Logged in visitors: 13 ; visits: 437310