OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Définition d'une famille de patrons de transformation pour l'analyse de modèles AADL

Renault, Xavier and Hugues, Jérôme Définition d'une famille de patrons de transformation pour l'analyse de modèles AADL. (2010) Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes (n° 93). ISSN 1265-1397

[img](Document in English)

PDF (Author's version) - Depositor and staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
308Kb

Abstract

AADL (Architecture Analysis and Design Language) est un langage de description d'architecture permettant une multitude d'analyses formelles ou semi-formelles, en utilisant par exemple des analyses statiques ou, encore, des techniques de model-checking. AADL fournit un niveau d'abstraction intéressant pour exprimer de nombreuses constructions utiles à la réalisation de systèmes embarqués temps réel. Parallèlement, nous remarquons que les propriétés à vérifier sur ces systèmes ne couvrent bien souvent qu'un sous-ensemble des éléments du modèle (composants ou propriétés non-fonctionnelles). Dans le présent article il est montré comment tirer parti de ces informations pour définir plusieurs patrons de transformation d'AADL vers les réseaux de Petri adaptés à la propriété à vérifier. Les propriétés qualitatives du système (comme la détection d'interblocage ou la traçabilité des messages échangés) peuvent être analysées à l'aide des réseaux de Petri colorés, en utilisant l'environnement CPN-AMI. Les propriétés quantitatives (comme l'ordonnancement du système ou la vérification du dimensionnement des tampons de communication) peuvent être traitées à l'aide des réseaux de Petri temporels, en utilisant l'environnement Tina. Les auteurs se sont intéressés à l'élaboration de patrons génériques pouvant être annotés en accord avec le type de propriété à traiter; ils montrent comment ces patrons permettent de limiter l'explosion combinatoire en restreignant le modèle à analyser aux seuls blocs utiles.

Item Type:Article
Additional Information:Thanks to Genie Industriel Multimedia editor : genie-logiciel@orange.fr
Audience (journal):Special issue journal
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE
Other partners > Université Pierre et Marie Curie, Paris 6 - UPMC (FRANCE)
Laboratory name:
Statistics:download
Deposited By:Jerome Hugues

Repository Staff Only: item control page