Analyse d'un modèle AADL à l'aide de Pola
HLADIK ; PERES ; XIAOMU
Type de document
COMMUNICATION AVEC ACTES INTERNATIONAL (ACTI)
Langue
francais
Auteur
HLADIK ; PERES ; XIAOMU
Résumé / Abstract
Cet article présente un travail mené sur l'intégration d'un langage formel de vérification, Pola, dans le processus de conception des systèmes temps réel critiques en se basant sur le langage AADL (Architecture Analysis and Design Language). Pola est un langage dédié qui permet de décrire le comportement de systèmes temps réel complexes en vue de leur vérification (ordonnançabilité, absence de blocages, etc), laquelle est effectuée par model checking. Le travail présenté consiste à utiliser les méthodes et outils de l'ingénierie des modèles pour transformer un modèle AADL vers un modèle Pola.
