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 metadatas

https://hal.univ-lorraine.fr/tel-01754324
Contributor : Thèses Ul <>
Submitted on : Friday, March 30, 2018 - 9:44:57 AM
Last modification on : Tuesday, April 24, 2018 - 1:30:04 PM

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

25

Files downloads

65