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

Autor: Zimmermann, Yann
Přispěvatelé: Proof-oriented development of computer-based systems (MOSEL), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Pierre-Yves Schobbens, Marie-Laure Potet and Pierre-Yves Schobbens and Hubert Toussaint and Germain Saval
Jazyk: francouzština
Rok vydání: 2007
Předmět:
Zdroj: Approches Formelles dans l'Assistance au Développement de Logiciels-AFADL'07
Approches Formelles dans l'Assistance au Développement de Logiciels-AFADL'07, Pierre-Yves Schobbens, Jun 2007, Namur, Belgique. pp.181-198
Popis: Les actes sont sur http://www.info.fundp.ac.be/~pys/AFADL07/Actes_AFADL_2007.pdf ; ISBN 978-2-87037-559-4; National audience; 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.
Databáze: OpenAIRE
Externí odkaz: