Développement formel de circuits électroniques par la méthode B

Yann Zimmermann 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Cet article expose une méthode de modélisation de circuits électroniques synchrones basée sur la méthode B événementielle. Dans ce formalisme adapté à la modélisation de systèmes, un circuit est modélisé par un ensemble d'événements. Certains principes de modélisation ont été dégagés pour l'application de la méthode à la modélisation de circuits synchrones. Un ensemble d'outils permet de valider par la preuve le modèle et ensuite d'obtenir le code simulable et synthétisable VHDL ou SystemC du circuit. Les différentes phases de modélisation sont illustrées à l'aide d'un exemple de protocole d'accès à un bus géré par un arbitre.
Type de document :
Communication dans un congrès
Marie-Laure Potet and Pierre-Yves Schobbens and Hubert Toussaint and Germain Saval. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07, Jun 2007, Namur, Belgique. Presses universitaires de Namur, pp.181-198, 2007, Actes de la 8e conférence AFADL - Approches Formelles dans l'Assistance au Développement de Logiciels
Liste complète des métadonnées

https://hal.inria.fr/inria-00172745
Contributeur : Dominique Cansell <>
Soumis le : lundi 17 septembre 2007 - 19:32:43
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Identifiants

  • HAL Id : inria-00172745, version 1

Collections

Citation

Yann Zimmermann. Développement formel de circuits électroniques par la méthode B. Marie-Laure Potet and Pierre-Yves Schobbens and Hubert Toussaint and Germain Saval. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07, Jun 2007, Namur, Belgique. Presses universitaires de Namur, pp.181-198, 2007, Actes de la 8e conférence AFADL - Approches Formelles dans l'Assistance au Développement de Logiciels. 〈inria-00172745〉

Partager

Métriques

Consultations de la notice

398