HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Assistance au développement incrémental et prouvé de systèmes enfouis

Abstract : Design process in electronic engineering is not formally defined and developments are based on empirical knowledge. Systems validation is made by tests but these are incomplete and all scenarios or use cases are not tested. We propose a design method built on proof and based on a case study, the RNRT project EQUAST, in the domain of digital television (DVB-T). Our works are based on refinement and its use helps tracability by distributing complexity in steps of refinement. The models help designer in his choices by structuring tasks of the system thanks to invariant properties and refinement. We propose a translation from models to SystemC code; produced code conserves properties of source models and helps to verify electronic constraints. Translation correction is proved by use of B event-based models which explain simulation semantics of SystemC. A specific SystemC program can be represented with a B model. This model is an instanciation of generic models describing SystemC simulation. With the help of refinement, we have shown that simulation of programs conserves properties of abstract models.
Document type :
Complete list of metadata

Contributor : Thèses Ul Connect in order to contact the contributor
Submitted on : Friday, March 30, 2018 - 9:44:57 AM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM


Files produced by the author(s)


  • HAL Id : tel-01754324, version 1



Cyril Proch. Assistance au développement incrémental et prouvé de systèmes enfouis. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2006. Français. ⟨NNT : 2006NAN10012⟩. ⟨tel-01754324⟩



Record views


Files downloads