Résumé: La technologie des systèmes mixtes matériels et logiciels connaît de nos jours une révolution sans pareille dans tous les domaines technologiques. Le fait de mélanger matériel et logiciel, ceci a donné naissance à des systèmes très complexes. La conception de tels systèmes, nécessite l’intervention de ressources humaine, financière et technologique très importante. Pour veiller au bon fonctionnement de leurs conceptions, ces systèmes doivent être soumis à des processus de validation très rigoureux. Une telle tâche n’est point évidente vue l’accroissement rapide de la complexité et de l’hétérogénéité des nouvelles architectures (matériel/logiciel). Aussi correcte que possible, la conception doit tenir compte de certaines propriétés dites critiques, qui sans leur présence risque d’engendrer une situation de catastrophe et même de ternir l’image de la compagnie. Dans ce travail, nous nous sommes intéressées à la mise en place d’un environnement intégré pour le développement des systèmes réactifs temps-réel. A cet effet, nous avons proposé plusieurs solutions pour la modélisation, la spécification et la vérification de plateformes matériel/logiciel. Dans un premier temps, nous avons utilisé une technique simple et efficace pour implémenter les diagrammes de décision binaire utilisés pour la représentation et la vérification des réseaux booléens symbolisant les systèmes réactifs. Nous avons ensuite, montré que l’axiomatisation des logiques temporelles linéaire LTL et arborescente CTL, permet de cerner de peu le problème de la complexité combinatoire spatio-temporelle. Les automates temporisés et la logique TCTL ont permis de mettre en place un modèle très utile pour la spécification et la vérification des systèmes temps réels. En se basant d’un coté sur la logique de réécriture comme modèle de spécification algébrique et philosophie universelle de raisonnement formel, et du système Maude comme outil de programmation et d’exécution de ces spécifications, nous avons intégré le tout en tant que noyau de programmation de l’environnement en question et sur lequel un ensemble de modules intégrés et spécialisés sont venus se greffer. Nous avons d’autant plus compris durant cette recherche, que la description UML et son extension UML/OCL et UML-RT, constituent pour le moment les meilleurs moyens pour la modélisation "semi-formelle" des systèmes réactifs temps-réel. Finalement, nous avons montré l’aisance même de l’utilisation de cet environnement à travers plusieurs exemples et benchmarks connus.

Batna:
Langue: Français
Collation: 179 p. ill. ;30 cm
Diplôme: Docteur Es Sciences
Etablissement de soutenance: Batna, Université El Hadj Lakhdar. Faculté des Sciences
Spécialité: Informatique
Index décimal 621.398 1 .Équipement informatique de communications et d'interfaçage (interfaces, matériels de communication et d'interfaces, multiplexage, techniques de transmission de données)
Thème Informatique

Mots clés:
Vérification de modèles (informatique)
ROBDD
UML/OCL
UML-RT

Note: Bibliogr. pp.160-173; Annexe pp.174-179