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 (93). ISSN 1265-1397
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 315kB |
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-SUPAERO (FRANCE) Other partners > Université Pierre et Marie Curie, Paris 6 - UPMC (FRANCE) |
Laboratory name: | Laboratoire d'Informatique de Paris 6 - LIP6 (Paris, France) - MoVe Département de Mathématiques, Informatique, Automatique - DMIA (Toulouse, France) - Modelisation et Architecture des Systèmes - MARS |
Statistics: | download |
Deposited On: | 07 Jul 2010 13:25 |
Repository Staff Only: item control page