Abstract FR:

La conception de systemes commence souvent par une phase de capture d'exigences, consistant a definir des comportements typiques attendus. Dans le domaine des applications distribuees, ces specifications incompletes sont le plus souvent donnees sous forme de chronogrammes ou scenarios, decrivant des communications entre entites du systeme. Cependant, la clarte d'un dessin ne leve pas toute ambiguite semantique, et le besoin d'outils d'analyse des exigences ainsi exprimees se fait rapidement sentir. De plus, les exigences contiennent deja suffisamment d'information pour envisager de verifier certaines proprietes formelles du systeme en construction. La these que nous defendons est qu'il est possible, grace a une modelisation par des scenarios, d'introduire des methodes formelles des la phase de capture des exigences d'un systeme distribue. Pour cela, nous etudions un langage de scenarios particulier, les high level message sequence charts (ou hmsc), et les manipulations formelles possibles a partir de ce langage muni d'une semantique. Dans un premier temps, nous proposons une semantique d'ordres partiels permettant de preserver l'aspect visuel du langage tout en facilitant sa manipulation formelle. Cette nouvelle semantique permet la definition d'une relation d'equivalence entre scenarios, ainsi qu'une simulation efficace des comportements definis. Une etude temporelle des hmsc est ensuite proposee, puis une technique de synthese automatique de code distribue.