|
|
Formal Tools for the
Virtual Prototyping
of Embedded Systems
|
Keywords
- virtual prototyping
- embedded systems,
- components,
- synchronous languages, engineering languages (SystemC, ...)
|
 |
Abstract
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.
|
|
