L'ampleur des systèmes informatiques, ainsi que leur complexité, se développent rapidement. Les systèmes ne sont plus utilisés séparément, mais sont généralement intégrés dans un contexte plus large, se connectant et interagissent avec plusieurs autres composants et systèmes. Ils deviennent ainsi beaucoup plus vulnérables aux erreurs : le nombre de défauts augmente de façon exponentielle avec le nombre de composants du système qui interagissent. En particulier, les phénomènes tels que la concurrence et le non-déterminisme qui sont au cœur de la modélisation des systèmes en interaction s'avèrent très difficiles à gérer avec des techniques standard. Leur complexité croissante, conjuguée à la pression pour réduire considérablement le temps de développement du système (« temps de mise sur le marché »), rend la livraison de systèmes informatique à faible défauts une activité extrêmement difficile et complexe. La fiabilité des systèmes informatiques est un problème majeur dans le processus de conception du système. Dans certains cas, ces erreurs de logiciel et de matériel ne menacent pas la vie des personnes mais elles peuvent avoir des conséquences financières importantes pour le fabricant.
La délivrance sur le marché d'un système informatique suppose donc au préalable que ce système doit être validé. Par conséquent, un défi majeur pour le domaine de l'informatique est de fournir des formalismes, des techniques et des outils qui permettront de concevoir efficacement des systèmes corrects et fonctionnels malgré leur complexité.
Au cours de la dernière décennie, de puissants outils ont été développés pour vérifier des spécifications de logiciel et de matériel. Il y a donc besoin de rendre accessible aux étudiants une formation de base qui leur permettra d'acquérir suffisamment des compétences pour pouvoir utiliser et raisonner dans de tels contextes.
- Enseignant: HARBOUCHE Ahmed