Les systèmes concurrents
La définition d'un système concurrent est celle, très générale, d'un logiciel ou d'une pièce d'équipement électronique dont la tâche à accomplir, modélisable à l'aide d'événements discrets, est divisée en plusieurs sous-tâches appellées processus. Ces processus coopèrent alors entre-eux de manière à accomplir collectivement le travail décrit par la tâche. Le terme coopération est ici très important car il permet de différencier les systèmes concurrents des systèmes parallèles dans lesquels les tâches sont indépendantes les unes des autres et dont le champ d'application est limité.
Les systèmes concurrents représentent un sujet de plus en plus étudié. Ils offrent a priori une solution simple au besoin croissant de performance en permettant de distribuer le travail à effectuer. La division des tâches complexes en processus simples permet également d'en simplifier tant la conception que la validation des composantes individuelles. L'arrivée récente de systèmes d'exploitations multi-tâches et multi-processeurs disponibles pour le grand public, ainsi que le nombre croissant de ceux-ci qui sont connectés à un réseau et qui sont capables d'implémenter des systèmes concurrents, ne fait que confirmer cette tendance.
Cependant, il y a lieu de se poser la question quant à savoir pourquoi l'usage des systèmes concurrents ne s'est pas rapidement répandu à toutes les couches d'utilisations des ordinateurs.
«Les systèmes concurrents sont complexes car les tâches qu'ils ont à effectuer sont également complexes.» [Mullender,89] La complexité inhérente des systèmes concurrents fait qu'il faut alors pouvoir vérifier que l'algorithme ou le programme qui les modélisent fait bien ce qu'il doit faire. Or dans les systèmes séquentiels traditionnels, la validation se faisait de manière séquentielle. On pouvait, en décomposant la tâche à effectuer en plusieurs actions élémentaires éxécutées en séquence, montrer si oui ou non cette tâche effectuait bien le travail qu'on voulait qu'elle fasse. De même, une simulation des données fournies au système et une analyse des résultats produits permettait de valider celui-ci.
Il n'en est pas ainsi dans les systèmes concurrents. On ne peut tout simplement pas prévoir à l'avance la séquence d'opérations qui sera éxécutée. Ceci fait que toute forme d'analyse séquentielle, ou même simulation, ne peut démontrer hors de tout doute qu'un système concurrent respecte bien une spécification donnée.
Or, sans méthodes de validation appropriées, l'utilisation des systèmes concurrents se montre risquée. On ne peut tout simplement pas se permettre que le comportement d'un système concurrent soit imprévisible, ou ne respecte pas sa spécification. Dans la pratique, de nombreux exemples de défaillances dues à des erreurs de modélisation de systèmes concurrents ont été répertoriés et analysés. Entre-autres:
Afin de valider avec certitude la spécification de systèmes concurrents, des méthodes d'analyse formelle apportant une certitude mathématique on été récemment développées. Elles permettent de décrire sans ambiguïté le comportement des systèmes en vérifiant que des propriétés telles que: "La ressource est utilisée par un seul processus à la fois", "Eventuellement, le processus sera disponible de nouveau" ou "Aucune donnée n'est perdue lors de la transmission", sont mathématiquement vraies ou fausses. Le succès relatif remporté par l'utilisation des méthodes formelles fait qu'elles commencent maintenant à être utilisées de manière autre que pédagogiques et débordent donc du cadre purement universitaire. Depuis peu, les grandes compagnies oeuvrant dans le domaine des systèmes concurrents commencent également à réaliser l'importance de ces méthodes et tentent d'en imposer l'utilisation.
Bien que la modélisation ne relève que des compétences de l'analyste, la validation quant à elle nécéssite en plus des logiciels spécialisés pouvant calculer mécaniquement les propriétées à valider. Chaque modèle possède donc ses propres outils de validation. Par exemple, les modèles suivants et un de leurs outils associés:
Un autre de ces modèles, celui que nous présentons, est celui des systèmes de transitions d'Arnold-Nivat. Le coeur même de ce modèle étant l'automate fini, il se présente donc comme un outil très naturel à utiliser parce qu'il contient explicitement les notions d'état et de transition, largement utilisées par les ingénieurs. Le fait que l'on travaille sur des graphes orientés nous permet également d'utiliser toutes les ressources de la théorie des graphes et d'implémenter ainsi de manière très efficace les calculs pratiques de propriétés.
Le résultat de cette implantation est le logiciel MEC. Il est assez puissant pour permettre l'analyse de systèmes concurrents industriels. Le prix de cette puissance repose sur des structures de données complexes et d'une optimisation poussée des algorithmes de calcul.
Le rôle de ce mémoire en est un d'initiation au modèle des systèmes de transitions d'Arnold-Nivat. Il montre au lecteur la complexité de l'implantation d'un logiciel comme MEC et de son utilisation dans des exemples pratiques.
Le chapitre I introduit les notions de base du modèle d'Arnold-Nivat d'un point de vue théorique. Le chapitre II définit une logique de systèmes de transitions permettant d'exprimer des propriétés relatives à ceux-ci. Le chapitre III est consacré entièrement à l'implantation pratique des concepts énoncés dans les deux chapitres précédents. Nous verrons ensuite au chapitre IV deux exemples complets d'utilisation du modèle d'Arnold-Nivat et du rôle joué par le logiciel MEC dans l'analyse de ceux-ci. Enfin, le chapitre V définira une nouvelle structure de gestion de graphes orientés, permettant une optimisation des performances d'éventuels successeurs de MEC.