Construction incrémentale vs. construction par raffinement de modèles comportementaux UML: sémantique et vérification des relations de spécialisation et d'implantation

Nous nous interessons aux demarches de construction de modeles comportementaux UML (machines d'etats) integrant des procedures de verification. Le raffinement, consistant a definir des specifications de plus en plus precises ou completes, n'a pu etre jusqu'a present formalise sur les machines d'etats. Dans les modeles orientes objets, la relation de raffinement peut se representer par la relation de specialisation. Nous proposons une semantique de la relation de specialisation entre machines d'etats UML. D'autre part, les techniques de construction incrementale visent a definir les realisations correspondant aux specifications elaborees tout au long du processus de conception. Cette correspondance se decrit par la relation d'implantation. Nous proposons egalement une semantique de cette relation entre machines d'etats UML. Ainsi, nous disposons d'outils permettant de mettre en \oe uvre des demarches incrementales et de raffinement en UML.