Ce projet fait partie du programme ARA SETIN
This project belongs to the ARA SETIN programme.



Formal Tools for the
Virtual Prototyping
of Embedded Systems


  • virtual prototyping
  • embedded systems,
  • components,
  • synchronous languages, engineering languages (SystemC, ...)
Version Francaise


In the context of past or current projects involving industrial partners from various application domains, the participants of FoToVP have observed several approaches for the design of complex and/or critical embedded systems, based on the notion of virtual prototyping. This allowed us to identify clearly where there is a need for formal tools. We started studying the benefits of formal methods and tools in the other projects, with the constraints of particular application domains, and with practical objectives in mind. Some recurring problems appeared, that need to be investigated further, independently of these application domains, and with less constraining short-term practical objectives. In this project called FoToVP, standing for ``Formal Tools for Virtual Prototyping of Embedded Systems'', we would like to study these recurring problems, in order to develop more fundamental and generic results. The motivations are clearly related to industrial applications, and the applicability of the project results will be evaluated with respect to these industrial practises and applications. The three application domains we have been studying in other projects, with industrial partners, are:
  • Systems-on-a-chip, with STMicroelectronics
  • Sensor networks, with FranceTelecom R&D
  • Embedded control systems, with EADS, Airbus, RATP,
In all these domains, we observed that the design of complex systems relies on the definition of a virtual prototype in the form of some executable high-level model of the system. This is made complex because such a model has to cover all elements of the embedded system, at various levels of abstraction: the hardware pieces, the software (both application software and operating system or middleware levels), the execution platform, and the physical environment. First, an executable model may be used extensively for simulations, to observe functional and non-functional properties of the system under construction. But, as these executable models appear first in the design flow, they become de facto reference models, and this raises several problems:
  • How can we build executable formal models of those complex systems, rich enough to be used as virtual prototypes?
  • What does it mean to validate properties formally on these models?
  • Since automatic implementation techniques from high-level models to effective software and hardware solutions usually do not exist yet (and will not exist soon), how can we compare a high-level reference model and a running implementation that is developed independently?
  • How can we express and validate non-functional properties of complex embedded systems on their high-level models, with some guarantee that these evaluations are realistic for the final running system?
To our opinion, the main points to be studied and integrated in a generic prototyping framework are:
  • Accurate modeling of physical environments and execution platforms
  • Extraction of rich executable formal models from non-formally defined prototyping languages like SystemC, Java, etc.
  • Automatic abstraction of these rich models, according to various criteria
  • Integration of external black-box code
  • Modeling of non-functional properties (non-functional time, energy, ...)
  • A general formal framework for functional and non-functional modular abstractions

Expected Scientific and Technical Outcomes

  • A global picture of virtual prototyping, from the formal point of view. We should define a global framework allowing to assemble several components that model the parts of a complex system (hardware, software, OS, ...). The semantics of the assemblage will take both functional and on functional aspects into account. We should also define a unified form of an individual component model for functional and non functional aspects, adequate for representing hardware pieces, but also the details of a piece of software, or some abstraction of the physical environment. Finally, we should define a ``more precise'' relationship on those individual components, to be able to deal with abstractions. The components and their assemblages witll be executable.
  • Tools for the extraction of formal models from engineering languages, and for the automatic abstraction of these models.
  • And, more generally, the progress of our knowledge on common problems and solutions, from various industrial application domains.

Expected Industrial and Economic Outcomes

On the industrial side, although we do not aim at providing directly usable results, the objectives of this project are inspired by industrial case studies. The generic and fundamental results we will develop in this project will then become a good starting point for more applied research work.