par 
Les systèmes embarqués sont si répandus qu’on ne les voit plus mais ils effectuent le gros des calculs aujourd’hui mettant en avant de nouveaux métiers et de nouveaux emplois comme « l’informatique embarquée» qui deviennent de par leur ampleur critiques pour la sécurité
Il est un fait certain dans le monde des IT que les logiciels et systèmes embarqués vont dominer la façon dont nous interagissons avec les ordinateurs et les calculs dans notre vie quotidienne. En effet, si l’on regarde de plus près, les ordinateurs ne sont plus des entités isolées, assis sur nos bureaux, au contraire et au lieu de cela, ils sont tissés, connectés et intégrés dans notre vie quotidienne via les gadgets que nous utilisons directement ou indirectement comme par exemple nos smartphones, nos démodulateurs pour télévision, nos machines à laver, le contrôle de notre voiture automobile ou les commandes d’un vol d’avion. Les systèmes embarqués sont si répandus qu’on ne les voit plus mais ils effectuent le gros des calculs aujourd’hui mettant en avant de nouveaux métiers et de nouveaux emplois comme « l’informatique embarquée» qui deviennent de par leur ampleur critiques pour la sécurité. Toutefois, tous n’ont pas la criticité élevée comme la nature des systèmes embarqués pour les automobiles, le contrôle des trains ou des rames de métro, les commandes de vol et les dispositifs médicaux ou d’autres. Cela ne veut pas dire que les systèmes embarqués ne sont pas critiques pour les téléphones mobiles, les contrôleurs pour des appareils ménagers (tels que machines à laver, micro-ondes et climatiseurs), démo et d’autres encore que l’on a chez soi et que nous utilisons tous les jours. Indépendamment de savoir si un système embarqué est critique ou non pour la sécurité, la nécessité d’intégrer la validation à chaque étape du flux de conception est primordiale. Il va de soi que pour la sécurité des systèmes embarqués critiques, il est nécessaire d’être plus rigoureux en termes de validation, et même lancer des preuves de programme, la simulation et l’analyse de performance. La vérification formelle se réfère à la vérification d’un système et de définir s’il se comporte comme prévu pour toutes les entrées possibles. Peut-on le faire avec des tests exhaustifs ? Là est la question posée par tous ceux qui font dans l’embedded. Traditionnellement, les méthodes de vérification formelles ont été utilisées pour donner des garanties mathématiques au sujet de la fonctionnalité d’un système. Cependant, pour donner des garanties strictes sur les performances (par exemple, donner une limite supérieure sur le temps d’exécution d’un logiciel donné), on a besoin d’employer des techniques d’analyse mathématiques pour estimer la performance. Ces techniques sont appelées l’analyse des performances. Un autre champ à explorer s’ouvre aux mathématiciens et informaticiens. Qui a dit que l’on n’a pas besoin de mathématiques ?
