Développement formel de circuits électroniques par la méthode B
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.