 |
 |
|
Les systèmes réactifs, c'est-à-dire les systèmes programmés en interaction continue avec leur environnement, sont de plus en plus courants, que ce soit comme composants de gros systèmes informatiques et de communication (e.g. les protocoles dans un réseau informatique), ou comme parties de systèmes de contrôle (e.g. l'informatique embarquée en aéronautique). De plus, le rôle de ces systèmes est souvent critique et leur défaillance peut avoir des conséquences économiques ou physiques sérieuses. Un développement de qualité est donc essentiel pour de tels systèmes. Il y a deux voies habituellement reconnues pour obtenir des développements de qualité dans ce contexte. La première, qui est déjà assez largement adoptée, est d'utiliser une méthodologie basée sur un langage de description de systèmes de haut niveau (e.g. SDL, les StateCharts,...) qui aide à systématiser et à documenter le processus de conception. De telles méthodologies sont souvent liées à des outils qui fournissent un support pour la capture et la documentation de la conception de systèmes. La seconde approche pour obtenir des développements de qualité est complémentaire à la première et fournit des outils pour analyser le résultat de la conception et pour vérifier qu'il satisfait les propriétés désirées. Lors du démarrage de ce projet, de nombreuses bonnes idées sur la manière de procéder à cette vérification existaient, mais leur exploitation pratique était encore rare.
La technique principale utilisée pour vérifier la conception de systèmes réactifs est l'exploration de l'espace des états et son extension plus souple, la vérification de modèles. L'avantage additionnel de la vérification de modèles est qu'elle permet l'utilisation de la logique temporelle, un langage expressif et commode pour exprimer les propriétés exigées, tout en préservant la possibilité d'utiliser des algorithmes relativement simples et faciles à implémenter pour vérifier que le système conçu vérifie les exigences imposées. L'inconvénient majeur de cette technique est qu'elle n'est directement applicable qu'à des systèmes dont l'espace des états à une taille limitée bien inférieure à ce que l'on voit habituellement en pratique. Ce projet visait à contribuer, et a contribué, à lever ce handicap. Les contributions issues du projet sont basées sur trois idées directrices.
La première est que simplifier le problème de l'analyse facilite la conception et l'implémentation de meilleurs algorithmes de vérification. La concrétisation de cette idée qui a été exploitée est que la vérification de modèles pour la logique temporelle peut être réduite à une simple exploration de l'espace des états en utilisant la traduction de formules en automates, objets qui peuvent être vus comme des représentations opérationnelles des formules.
La seconde ligne directrice est d'attaquer les causes de la taille souvent excessive de l'espace des états. Le projet a montré que cela était possible en ce qui concerne l'explosion de l'espace des états venant de la modélisation du parallélisme par l'entrelacement. En effet, en analysant soigneusement l'interaction des actions des activités concurrentes, il est possible de se limiter à explorer certains de leurs entrelacements tout en permettant une analyse complète
La dernière idée directrice est que l'usage bien pensé de techniques algorithmiques avancées peut mener à des améliorations substantielles. Ce point de vue a été appliqué au problème de la représentation et de la mémorisation d'espaces d'états. Ce problème a été choisi parce que les données expérimentales montrent que la quantité de mémoire excessive nécessaire à la conservation de l'espace des états est une des causes les plus fréquentes de l'échec des tentatives de vérification. La technique utilisée est une application originale de la technique du "hashing" vue comme méthode de compression.
En plus d'un bon nombre de publications dans des congrès et revues internationaux, le projet a produit des implémentations de ses nouvelles techniques principales. Ces implémentations ont été réalisées dans le contexte de l'outil SPIN et ont été largement évaluées et adoptées. En conclusion, on peut dire que le projet a contribué significativement à l'évolution rapide de l'état de l'art de la vérification des systèmes réactifs. Ses contributions ont été bien reçues dans le milieu international de la recherche. De plus, le projet a contribué à développer une expertise locale qui devrait se révéler de grande valeur lorsque les techniques de vérification, qui maintenant sont devenues plus facilement applicables, seront plus largement adoptées dans le monde industriel.
|
|
|