QUARTEFT

Les nouvelles chaînes de développement de systèmes critiques reposent sur des langages de modélisation spécifiques au métier ciblé et sur des transformations qualifiées (assurance que la transformation préserve les propriétés d’intérêts) entre langages. Le projet FIESTA vise à développer les technologies pour faciliter cette approche dans le contexte des systèmes embarqués temps-réel. Il s’appuie d’une part sur la définition de langages pivots dédiés et sur l’exploitation de techniques formelles pour prouver la correction des transformations. L’étude proposée s’appuie sur le langage FIACRE, un des langages pivots pour la vérification formelle des aspects temps-réel dans le projet TOPCASED (http://www.topcased.org/) ; il factorise et optimise la chaîne de traduction entre les langages "métier" tels que SDL, AADL, ... et les outils de vérifications de modèles tels que TINA et CADP. Cette proposition vise à renforcer cette approche sur deux aspects complémentaires : d'une part, définir des extensions de FIACRE lui permettant de prendre en compte de façon native des concepts de haut niveau tels que les modes, les notions de partitionnement temporel, les constructeurs temps-réel; et d'autre part développer les techniques de validation et vérification des transformations de FIACRE étendu (nommé RT-FIACRE) vers FIACRE et les outils de vérification pour disposer d'une chaîne sûre complète allant des outils de modélisation métier aux outils de
vérifications.