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
Theses

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 :
Theses
Complete list of metadata

https://hal.univ-lorraine.fr/tel-01754324
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

File

SCD_T_2006_0012_PROCH.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01754324, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

29

Files downloads

139