Skip to Main content Skip to Navigation

Modélisation et développement formel de circuits électroniques

Abstract : Electronics systems become more and more complex and reliability requirements are more and more important. The challenge is to continue to develop more and more complex systems while ensuring correction of systems. Test-based methods are now overtaken by complexity of systems. We suggest using proof and refinement to ensure correction of systems. Proof-based methods are not limited by the complexity of systems. We suggest using the B method and its concept of refinement to simplify the process of modelling and proving. At each refinement step, proof obligations are automatically generated by tools to ensure that the concrete model is correct with respect to the abstract model. This method ensures that the final implementation is correct with respect to the initial abstract model which is the specification. We started by a realistic case study chosen by an industrialist (Volvo) consisting in modelling an access controller for a serial bus. This case study leaded us to define some modelling rules to develop electronic circuits using the B method. We have defined the BHDL language which is the synthesisable level of B and we have implemented translators from BHDL towards VHDL and SystemC. A theoretic study of BHDL has been done defining two semantics for this language and proving the correction for the translation from BDHL to VHDL. Some work has also been done to translate BHDL to ACL2.
Document type :
File URL :
Complete list of metadata
Contributor : Thèses Ul <>
Submitted on : Friday, March 30, 2018 - 9:43:18 AM
Last modification on : Wednesday, March 11, 2020 - 2:08:36 PM


  • HAL Id : tel-01754271, version 1



Yann Zimmermann. Modélisation et développement formel de circuits électroniques. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2006. Français. ⟨NNT : 2006NAN10213⟩. ⟨tel-01754271⟩



Record views