Notice
Aspects temporels dans les systèmes embarqués critiques
- document 1 document 2 document 3
- niveau 1 niveau 2 niveau 3
Descriptif
La plupart des systèmes embarqués que l'on trouve dans les applications critiques telles que les commandes de vol d'un avion ou le contrôle d'un moteur ou de l'ABS dans une automobile, font intervenir des aspects temporels. Ces derniers compliquent leur conception et leur réalisation lorsqu'il faut assurer qu'ils ont un comportement sûr (de fonctionnement). Afin d'atteindre ce but plusieurs phases, qui doivent être cohérentes, sont nécessaires.
La première phase consiste à effectuer une spécification fonctionnelle, souvent appelée modélisation, du système ou seuls les aspects fonctionnels et/ou causalité sont considérés. Cela permet de faire un premier niveau de vérification en termes d'ordre sur les événements qui entrent et sortent du systèmes relativement à un temps logique (sémantique des langages synchrones). Ce dernier fait l'hypothèse que l'on ne s'intéresse pas au temps physique nécessaire pour exécuter les fonctions. Cette première spécification doit s'accompagner d'une spécification non fonctionnelle dont l'objet est de donner, maintenant, des caractéristiques temporelles physiques aux différentes fonctions, pouvant ou non dépendre de l'architecture matérielle sur lesquelles elles s'exécuteront, et de décrire cette architecture. Dans le cas le plus général cette dernière est formée de plusieurs processeurs pouvant être de types différents, plusieurs circuits intégrés spécifiques réalisant chacun une fonction unique, tous ces composants échangeant des données à l'aide de moyens de communications pouvant, eux aussi, être de types différents.
La deuxième phase consiste à faire une analyse d'ordonnançabilité temps réel (temps physique) dont l'objet est double : montrer que la combinaison de la spécification fonctionnelle et non fonctionnelle peut conduit à une solution ordonnaçable sur l'architecture matérielle et synthétiser cet ordonnancement. Cette analyse d'ordonnançabilité doit bien sûr tenir compte des vérifications effectuées en temps logique.
La dernière phase consiste à transformer le résultat de la phase précédente en un code exécutable par les processeurs et les circuits intégrés spécifiques formant l'architecture matérielle. Cela conduit à générer automatiquement soit des mécanismes de synchronisation dans le cas d'architecture déclanchées par des événements, soit des appels à des fonctions dans le cas d'architecture déclanchées par le temps. Cette approche permet de concevoir et réaliser des systèmes embarqués critiques sûrs par construction.
Thème
Dans la même collection
-
Explorations Mathématiques de l'activité du cerveau
TouboulJonathanExplorations Mathématiques de l'activité du cerveau Le siècle dernier a été une période fascinante durant laquelle les recherches expérimentales ont fait des avancées majeures sur la
-
Logic-based static analysis for the verification of programs with dynamically allocated data struct…
DrăgoiCezaraSoftware development has reached a complexity level that cannot be handled without the aid of computer assisted methods. It is therefore of the highest importance to have rigorous methods and
-
Resolving Entities in the Web of Data
ChristophidesVassilisOver the past decade, numerous knowledge bases (KBs) have been built to power a new generation of Web applications that provide entity-centric search and recommendation services. These KBs offer
-
Wireless In the Woods: Monitoring the Snow Melt Process in the Sierra Nevada
WatteyneThomasHistorically, the study of mountain hydrology and the water cycle has been largely observational, with meteorological forcing and hydrological variables extrapolated from a few infrequent manual
-
Phénomènes Aléatoires dans les Réseaux
RobertPhilippeLes phénomènes aléatoires sont une composante-clé des réseaux de communication, ils interviennent, de façon majeure, dans le trafic que les réseaux traitent, ainsi que dans certains algorithmes
-
Modèles mémoire pour les multiprocesseurs à mémoire partagée
MarangetLucLa plupart des systèmes qui s'apparentent à des ordinateurs un tant soit peu sophistiqués comprennent plusieurs unités de calcul qui communiquent par l'intermédiaire d'une mémoire partagée.
-
Gestion de données personnelles respectueuse de la vie privée
AnciauxNicolasEn très peu de temps, nous sommes entrés dans une ère de génération massive des données personnelles créées par les individus, leurs équipements digitaux ou mises à disposition par certaines
-
Génération de maillages pour la simulation numérique
LoseilleAdrienUne branche importante du calcul scientifique consiste à simuler sur ordinateurs des phénomènes physiques complexes. Son intérêt consiste à mieux appréhender des problèmes fondamentaux : solution
-
Réseau optiques, algorithmes et probabilités
RobertsJ. B.L'objectif des recherches de l'équipe RAP est de modéliser le comportement de réseaux de divers types, soumis à une demande de nature aléatoire, afin la prédire leurs performances. Le partage des
-
Réduction de modèles de voies de signalisation intracellulaire
FeretJérômeLes voies de signalisation intracellulaire sont des cascades d'interaction entre protéines, qui permettent à la cellule de recevoir des signaux, de les propager jusqu'à son noyau, puis de les