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.
Mot(s) clés libre(s) : système embarqué