Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Modélisation algorithmique et synthèse d'architectures assistées par model-checking

Jean-Christophe Le Lann 1 Philippe Dhaussy 1 Pierre-Laurent Lagalaye
1 Lab-STICC_ENSTAB_CACS_MOCS ; IDM
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192), STIC - Pôle STIC [Brest]
Résumé : L'ingéenierie des architectures logicielles basée sur le prototypage rapide conduit à des itérations nombreuses dont le coût en simulation ne peut être néegligé. Ceci se révèle particulièrement crucial pour les applications multimédia (encodeurs, décodeurs vidéo, etc), qui cumulent des spéci- cités de flux de données, de contrôle et de traitements complexes, découpés en automates à grains fins. Les outils de modélisation HW/SW de telles applications sou ffrent donc d'une forme d'incompatibilité entre les ambitions en terme de prototypage et les besoins en tests incessants, consommateurs de temps. L'utilisation des techniques de véri fication formelle par "model-checking" constitue une solution à cette incompatibilité notoire. Nous décrivons dans cet article un travail exploratoire qui étudie l'association d'un outillage original de modélisation d'architectures mixtes logiciel matériel basé sur le langage Ruby avec un outil de véri fication, nommé OBP (Observer-Based Prover), basé sur les observateurs. Nous illustrons notre contribution par un exemple et décrivons des résultats sur les preuves d'exigences menées.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal-ensta-bretagne.archives-ouvertes.fr/hal-00703785
Contributeur : Annick Billon-Coat <>
Soumis le : lundi 4 juin 2012 - 13:26:31
Dernière modification le : mercredi 24 juin 2020 - 16:19:23

Identifiants

  • HAL Id : hal-00703785, version 1

Citation

Jean-Christophe Le Lann, Philippe Dhaussy, Pierre-Laurent Lagalaye. Modélisation algorithmique et synthèse d'architectures assistées par model-checking. CAL 2012-, May 2012, Montpellier, France. ⟨hal-00703785⟩

Partager

Métriques

Consultations de la notice

378