Modélisation algorithmique et synthèse d'architectures assistées par model-checking
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.