Approche avec B (Y. Aït-Ameur) ------------------------------ Notre approche consiste a representer une IHM comme un systeme de transitions entre etats. Les etats regroupent des proprietes (attributs) de l'IHM, proprietes qui sont extraites du cahier des charges. La formalisaion en B consiste donc a decrire les etats, et les operations des machines B permettant de representer les transitions entre etats. Le principe est celui des plus faibles preconditions. Si S est une action et Q une propriete a etablir, alors [S]Q est la plus faible precondition qui permet d'etablir Q. Notons la P et appelons [s]P une substitution generalisee. JR Abrial a defini ainsi un calcul inductif sur les substitutions generalisees. Ainsi, si nous souhaitons qu'une propriete donnee R soit satisfaite par une operation OP, il suffit que cette operation ait pour precondition [OP]R. Cette derniere est une obligation de preuve que le prouveur devra decharger. Autre exemple, un invariant I doit etre maintenu par toutes les operations et donc toutes les OPi doivent avoir une precondition a TRUE. Ainsi il faudra etablir [OPi]I. Ces points constituent la base de notre approche. Nous avons a l'aide de ce mecanisme formaliser une specification des l'etude de cas des PostIts, formilser certaines proprietes liees aux interfaces, formaliser le developpement jusqu'au code ADA-TCL TK. Notons que notre approche est completement outillee et ne constitue pas un travail papier. Enfin, actuellement nous explorons la possibilite d'effectuer de la validation des specifications B. En effet, nous ne sommes pas capables aujourdhui d'effectuer des tests de validation. Mais, certains premiers resultats non encore publies nous permettent d'envisager cette possibilite dans un futur proche. Notre presentera tentera de resumer ces differents points.