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

Les méthodes de développement rigoureuses ne se sont pas encore imposées en électronique. La validation des systèmes se fait par des séries de tests ou par l'utilisation de model checker ne couvrant pas toutes les possibilités. Nous avons élaboré une méthode de développement par la preuve en nous appuyant sur une étude de cas (TV numérique). Le raffinement est central à nos travaux car il permet de conserver la traçabilité et distribue la complexité du système et des preuves. Les modèles construits aident aux choix architecturaux en structurant les tâches du système. Nous avons proposé un mécanisme de traduction de modèles produisant du code SystemC. Le code obtenu sert de support aux expérimentations électroniques. La traduction est prouvée par des modèles B décrivant la sémantique de simulation SystemC. Un programme est représenté par un modèle B, instanciation des modèles de simulation. Nous montrons que l'exécution des programmes traduits conservent les propriétés des modèles.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.NANCY1-SCD Sciences & Techniques (545782101) / SudocSudocFranceF