Parmi les modules proposés dans la deuxième année du Master « Informatique et Traitement d’Information » à l’Ecole Supérieure d’Ingénieurs d’Annecy, le module enseigné par M. Flavio Oquendo intitulé « Conception logicielle de systèmes surs & Ingénierie des logiciels distribués ». Ce module m’a permis d’améliorer mes connaissances dans la modélisation et le développement des systèmes critiques, distribués en temps réel.

La conception et la construction de ce type d’applications de plus en plus complexes et mobiles passe par une modélisation rigoureuse. On a besoin de représenter d’une façon simplifiée le système, modéliser son comportement, les interactions internes entre ces différents composants et les interactions avec l’environnement surtout lorsqu’il s’agit d’un système embarqué qui demande un haut niveau de sécurité et de fiabilité.

Aussi on a besoin de vérifier et de valider le fonctionnement du système. La phase de test permet sans aucun doute de détecter quelques erreurs et de vérifier, dans certaines limites, la qualité du système, mais c’est sur que cette étape n’est pas suffisante vu qu’elle ne permet pas d’identifier tout les ‘bugs’. C’est pour cela qu’on a besoin d’aller plus loin, vers une ingénierie système basé sur des preuves : établir des propriétés (sûreté, vivacité) et de les vérifier, gérer les interférences, éviter l’interblocage (Deadlock), synchroniser les communications, utiliser les techniques de simulation, répartir d’une manière dynamique les ressources et les systèmes, etc …

Cette approche fondée sur la modélisation et la programmation concurrente des systèmes critiques permet de définir d’une façon claire et non ambiguë la structure du système. Par exemple la modélisation en LTS (Labeled Transition System) exprimée en FSP (Finite State Process) avec l’utilisation des outils d’animation et de vérification de propriétés tels que LTSA (LTS Analyzer Tools). Enfin traduire ou bien générer le code équivalent tout en respectant les modèles déjà spécifiés et validés.