Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00172745
Contributor : Dominique Cansell <>
Submitted on : Monday, September 17, 2007 - 7:32:43 PM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM

Identifiers

  • HAL Id : inria-00172745, version 1

Collections

Citation

Yann Zimmermann. Développement formel de circuits électroniques par la méthode B. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07, Pierre-Yves Schobbens, Jun 2007, Namur, Belgique. pp.181-198. ⟨inria-00172745⟩

Share

Metrics

Record views

520