Abstract FR:

Actuellement il est toujours difficile de specifier le fonctionnement d'un systeme interactif a cause de la complexite du dialogue entre l'homme et le systeme. Il existe a ce niveau une dualite et un fosse entre la prise en compte des facteurs humains et techniques. Notre travail se situe a la croisee du genie logiciel et de l'interaction homme-machine afin d'obtenir un cadre federateur permettant le developpement rigoureux de systemes interactifs a l'aide d'une approche de type genie logiciel. Dans la premiere partie nous proposons une methodologie d'evaluation des formalismes dediee a l'interaction homme-machine. Cette evaluation s'effectue a l'aide d'une vingtaine de criteres qui permettent de cerner les forces et les faiblesses d'un formalisme. Liee a cette evaluation, nous proposons une taxonomie des differents formalismes que nous avons testes. Ces deux metriques permettent de replacer l'evaluation d'un formalisme par rapport aux influences qui ont permis sa conception. Cette etude nous a servi pour valider les concepts fondateurs du formalisme xtl elabore dans la deuxieme partie. Xtl est une logique temporelle etendue dediee a la specification des systemes interactifs qui a ete concue au depart pour privilegier l'expressivite dans le cadre d'une semantique rigoureuse. Le modele de xtl est un modele a plusieurs chemins d'execution qui permet notamment l'expression des interruptions et de la concurrence. Il en resulte un langage avec lequel on peut modeliser des problemes complexes ou peuvent intervenir, entre autres, erreurs humaines, interruptions, concurrence et temps reel. Par la suite, nous proposons une classification des proprietes d'interet relatives aux systemes interactifs. Nous montrons notamment comment exprimer les proprietes de robustesse comme l'observabilite, l'insistance ou l'honnetete. Il ressort de cette etude que la plupart des proprietes sont exprimables sous la forme de proprietes simples de la classe de l'observabilite. Finalement, l'etude de cas proposee permet d'avoir une vue d'ensemble de l'utilisation du formalisme sur un cas concret : un systeme de supervision destine a la gestion d'un reseau d'automates de banques. Nous montrons en particulier comment implanter puis formaliser la notification.