Transformation de modèles UML vers Fiacre, via les langages intermédiaires tUML et ABCD

International audienceLa complexité des systèmes embarqués continue d'augmenter. Leur développement nécessite donc un processus de développement rigoureux pour répondre aux normes de certification très strictes. Dans ce contexte l'utilisation des méthodes formelles pour la vérification promet des gains importants en termes de fiabilité et temps de développement. En revanche, le fossé sémantique entre les langages utilisés par le domaine industriel et ceux pris en compte par les outils formels est une barrière réelle pour l'adoption de ces derniers. Dans cet article, nous introduisons une chaîne de transformation modulaire permettant l'obtention de modèles formels à partir d'un formalisme d'entrée basé sur UML. Les modèles ainsi obtenus permettent la vérification de propriétés