ur des applications diverses et variées utilisées dans la vie
courante telles que les télécommunications (téléphonie/Internet
mobile, services réseaux, ...), la bureautique et l'électroménager
(PDA, set-top boxes, ...), les opérations bancaires (cartes à puces,
guichets automatiques, ...), les transports (systèmes de conduite ou
de guidage automatique, contrôle aérien, ...), etc.
La compléxité grandissante de ces applications et l'émergence de standards internationaux (par exemple, http://java.sun.com/products/javacard/Java Card (TM) pour les cartes à puces, http://www.rtj.org/Real-Time Specification for Java, pour les systèmes temps-réel) est en train de pousser les industriels des domaines concernés à faire appel à des langages de programmation de haut-niveau, tels que JAVA ou C++. Cette tendance est motivée par les multiples avantages de ces langages, citons en particulier, l'approche orientée objet, qui permet le développement rapide et la définition de composants réutilisables et évolutifs, et l'indépendance de la plate-forme d'exécution, qui permet le déploiement de la même application sur différentes architectures cibles.
La plupart des logiciels embarqués font partie des systèmes critiques. En effet, toute défaillance dans le respect des contraintes de fonctionnement peut entrainer des conséquences économiques, écologiques et/ou humaines considérables. Ceci rend nécessaire le développement de méthodes et d'outils de conception pour valider le respect des exigences. De telles méthodes doivent comprendre des techniques de vérification automatique permettant d'une part de (1) détecter les comportements défectueux d'un système, et d'autre part de (2) vérifier que tous les comportements d'un système sont conformes à ses spécifications.
Le développement de techniques et d'outils de vérification automatique pour les logiciels embarqués, et pour les systèmes logiciels de manière générale, constitue depuis plusieures années l'un des thèmes de recherche majeurs dans le domaine des technologies du logiciel.
Toutefois, la programmation de logiciels embarqués avec des langages comme JAVA, introduit dans le panorama scientifique des nouveaux problèmes difficiles, liés notamment à l'utilisation du multi-threading, de la récursion et de la mémoire dynamique, trois mécanismes jusqu'à lors interdits par les pratiques industrielles (notamment toutes celles nécessitant d'une qualification ou certification conforme aux standards de sûreté de fonctionnement logiciel en vigueur pour le domaine industriel concerné - DO178-B, EN-50128, IEC-880 etc..) et mal couverts par les méthodes et outils de vérification automatique.