La vérification automatique de ce nouveau type de logiciels embarqués
pose de nombreux problèmes non triviaux aussi bien sur le plan
théorique et méthodologique (modélisation et automatisation de la
vérification) que sur le plan pratique (mise en 
uvre et passage à
l'echelle).
Les outils existants de vérification basée sur les modèles (model-checking), tels que SPIN [#!spin!#], SMV [#!smv!#], IF [#!if!#], KRONOS [#!kronos!#], etc., ont été développés pour traiter des systèmes dont l'essentiel du comportement n'est pas de transformer des données (et donc ne dépend pas des données), et dont le contrôle peut être énorme mais fini. Ceci est bien adapté pour raisonner par exemple sur les systèmes matériels (circuits booléens) ou les protocoles de communication, à un certain degré d'abstraction.
Des travaux récents ont étendu le champ d'application des outils de vérification automatique à des classes de logiciels embarqués, notamment synchrones, dont le comportement est dominé soit par le contrôle ou soit par les données, mais où l'interaction entre eux est très faible. C'est le cas par exemple de l'outil Taxys qui permet la vérification des propriétés temporelles sur le temps d'exécution d'un programme Esterel sur une architecture mono-processeur [#!taxys!#].
Or, les logiciels comportant du multi-threading, de la récursion et/ou de la mémoire dynamique, ne rentrent pas dans le cadre proposé par les techniques de vérification actuelles. En effet, leur comportement dépend fortement d'aspects dont il est difficile de s'abstraire sans une perte significative en précision dans la modélisation et l'analyse.