%0 Journal Article
%T Transformation de modèles UML vers Fiacre, via les langages intermédiaires tUML et ABCD
%+ ESEO-TRAME (TRAME)
%+ Lab-STICC_ENSTAB_ CACS_MOCS
%+ Institut de Recherche en Communications et en Cybernétique de Nantes (IRCCyN)
%A Jouault, Frédéric
%A Teodorov, Ciprian
%A Delatour, Jérôme
%A Le Roux, Luka
%A Dhaussy, Philippe
%< avec comité de lecture
%@ 1265-1397
%J Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes
%I Génie industriel multimédia
%V 109
%P xx
%8 2014-06-02
%D 2014
%K modélisation
%K model-checking
%K systèmes embarqués
%K UML
%Z Computer Science [cs]/Symbolic Computation [cs.SC]
%Z Computer Science [cs]/Software Engineering [cs.SE]
%Z Computer Science [cs]/Modeling and Simulation
%Z Computer Science [cs]/Embedded SystemsJournal articles
%X La 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.
%G English
%L hal-01006656
%U https://hal.science/hal-01006656
%~ UNIV-BREST
%~ UNIV-NANTES
%~ INSTITUT-TELECOM
%~ ENSTA-BRETAGNE
%~ CNRS
%~ UNIV-UBS
%~ EC-NANTES
%~ IRCCYN
%~ IRCCYN-STR
%~ ENSTA-BRETAGNE-STIC
%~ UNAM
%~ ENIB
%~ LAB-STICC
%~ ESEO-TECH
%~ ESEO-TRAME
%~ TDS-MACS
%~ INSTITUTS-TELECOM
%~ ESEO-ERIS
%~ NANTES-UNIVERSITE
%~ UNIV-NANTES-AV2022
%~ NU-CENTRALE