F. La-figure, 15 présente le schéma de la seconde stratégie de preuve d'inclusion des traces entre les différents niveaux. Nous avons généré directement les modèles abstraits des niveaux en gardant que les actions du NIVEAU_0 observables dans le but de répondre au problème d'explosion combinatoire

]. F. Bibliographie1, E. Abbes, M. Casseau, and . Abid, Spécification et conception de systemes sur puce avec SystemC, Etude de cas : le turbo-codage. RenPar'15, 2003.

J. Abrial, The B-book : assigning programs to meanings, 1996.
DOI : 10.1017/CBO9780511624162

J. Abrial, Modeling in Event-B : System and Software Engineering, 2010.
DOI : 10.1017/CBO9781139195881

C. André, Le temps dans le profil UML MARTE, 2007.

J. Andronick, B. Chetali, and C. Paulin-mohring, Formal Verification of Security Properties of Smart Card Embedded Source Code, FM, Lecture Notes in Computer Science, pp.302-317, 2005.
DOI : 10.1007/11526841_21

L. Apvrille, W. Muhammad, R. Ameur-boulifa, S. Coudert, and R. Pacalet, Abstract application modeling for system design space exploration, Euromicro conference on Digital System Design (DSD 06), 2006.
URL : https://hal.archives-ouvertes.fr/hal-00525081

K. Bae, P. C. Ölveczky, T. H. Feng, E. A. Lee, and S. Tripakis, Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude, Science of Computer Programming, vol.77, issue.12, pp.1235-1271, 2012.
DOI : 10.1016/j.scico.2010.10.002
URL : http://dx.doi.org/10.1016/j.scico.2010.10.002

F. Balarin, M. Chiodo, P. Giusto, H. Hsieh, A. Jurecska et al., Hardwaresoftware co-design of embedded systems : the POLIS approach, 1997.

F. Balarin, Y. Watanabe, H. Hsieh, L. Lavagno, C. Passerone et al., Metropolis: an integrated electronic system design environment, Computer, vol.36, issue.4, pp.45-52, 2003.
DOI : 10.1109/MC.2003.1193228

J. Baumgartner and T. Heyman, An overview and application of model reduction techniques in formal verification, 1998 IEEE International Performance, Computing and Communications Conference. Proceedings (Cat. No.98CH36191), pp.165-171, 1998.
DOI : 10.1109/PCCC.1998.659939

I. Beer, S. Ben-david, C. Eisner, D. Geist, L. Gluhovsky et al., RuleBase: Model checking at IBM, Computer Aided Verification, pp.480-483, 1997.
DOI : 10.1007/3-540-63166-6_53

F. Bellegarde, J. Julliand, and O. Kouchnarenko, Ready-Simulation Is Not Ready to Express a Modular Refinement Relation, the Third Internationsl Conference on Fundamental Approaches to Software Engineering, FASE'00, pp.266-283, 2000.
DOI : 10.1007/3-540-46428-X_19

N. Benaissa and D. Méry, Proof-Based Design of Security Protocols, 5th International Computer Science Symposium in Russia, pp.25-36, 2010.
DOI : 10.1007/978-3-642-13182-0_3
URL : https://hal.archives-ouvertes.fr/inria-00542919

B. Berthomieu, J. Bodeveix, S. Dal-zilio, P. Dissaux, M. Filali et al., Formal Verification of AADL models with Fiacre and Tina, Embedded Real-Time Software and Systems, ERTSS 2010, pp.1-9, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00494348

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, Symbolic Model Checking Using SAT Procedures instead of BDDs, Proceedings of the 36th annual ACM/IEEE Design Automation Conference, DAC'99, pp.317-320, 1999.

A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, Bounded model checking Advances in computers, pp.117-148, 2003.

A. Bouali, A. Ressouche, V. Roy, and R. Simone, The Fc2tools set, Algebraic Methodology and Software Technology, pp.595-598, 1996.
DOI : 10.1007/BFb0014350

T. Boulusset, ?-SPACE : Raffinement de descriptions architecturales en machines abstraites de la méthode formelle B, 1992.

C. Braunstein and E. Encrenaz, Using CTL formulae as component abstraction in a design and verification flow, Seventh International Conference on Application of Concurrency to System Design (ACSD 2007), pp.80-89, 2007.
DOI : 10.1109/ACSD.2007.76
URL : https://hal.archives-ouvertes.fr/hal-01305787

R. Brayton, G. Hachtel, A. Sangiovanni-vincentelli, F. Somenzi, A. Aziz et al., VIS: A system for verification and synthesis, Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pp.428-432, 1996.
DOI : 10.1007/3-540-61474-5_95

J. Brunel, E. A. Kock, W. M. Kru?tzer, H. J. Kenter, and W. J. Smits, Communication refinement in video systems on chip, Proceedings of the seventh international workshop on Hardware/software codesign , CODES '99, pp.142-146, 1999.
DOI : 10.1145/301177.301511

L. Cai, S. Verma, and D. Gajski, Comparison of SpecC and SystemC Languages for System Design, 2003.

J. P. Calvez, Embedded real-time systems. A specification and design methodology, 1993.

D. Cansell, G. Gopalakrishnan, M. Jones, D. Méry, and A. Weinzoepflen, Incremental Proof of the Producer/Consumer Property for the PCI Protocol, 2nd International Conference of B and Z Users, pp.22-41, 2002.
DOI : 10.1007/3-540-45648-1_2
URL : https://hal.archives-ouvertes.fr/inria-00100888

D. Cansell, D. Méry, and C. Proch, System-on-chip design by proof-based refinement, International Journal on Software Tools for Technology Transfer, vol.7, issue.1, pp.217-238, 2009.
DOI : 10.1007/s10009-009-0104-7
URL : https://hal.archives-ouvertes.fr/inria-00426385

H. Cho, S. Abdi, and D. Gajski, Interface synthesis for heterogeneous multi-core systems from transaction level models, Proceedings of the 2007 ACM SIGPLAN/- SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, pp.140-142, 2007.

E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '83, pp.117-126, 1983.
DOI : 10.1145/567067.567080

E. M. Clarke, A. Gupta, and O. Strichman, SAT-Based Counterexample-Guided Abstraction Refinement, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.23, issue.7, pp.1113-1123, 2004.
DOI : 10.1109/TCAD.2004.829807
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.91.2429

J. L. Colley, Guarded Atomic Actions and Refinement in a System-on-Chip Development Flow : Bridging the Specification Gap with Event-B, 2010.

P. Coussy, Synthèse d'interface de communication pour les composants virtuels, 2003.

P. Coussy, E. Casseau, P. Bomel, A. Baganne, and E. Martin, A formal method for hardware IP design and integration under I/O and timing constraints, ACM Transactions on Embedded Computing Systems, vol.5, issue.1, pp.29-53, 2006.
DOI : 10.1145/1132357.1132359
URL : https://hal.archives-ouvertes.fr/hal-00077860

P. Coussy, C. Chavet, P. Bomel, D. Heller, E. Senn et al., GAUT: A High-Level Synthesis Tool for DSP Applications, High-Level Synthesis, chapter 9, pp.147-169, 2008.
DOI : 10.1007/978-1-4020-8588-8_9
URL : https://hal.archives-ouvertes.fr/hal-00489794

J. Dekeyser, A. Gamatié, S. Meftali, and I. R. Quadri, Models for Co-design of Heterogeneous Dynamically Reconfigurable SoCs, Heterogeneous Embedded Systems -Design Theory and Practice, p.26, 2011.
DOI : 10.1007/978-94-007-1125-9_6
URL : https://hal.archives-ouvertes.fr/inria-00525023

D. Densmore and R. Passerone, A Platform-Based Taxonomy for ESL Design, IEEE Design & Test of Computers, vol.23, issue.5, pp.359-374, 2006.
DOI : 10.1109/MDT.2006.112

E. W. D?kstra, A Discipline of Programming, 1976.

C. Erbas, System-Level Modeling and Design Space Exploration for Multiprocessor Embedded System-on-Chip Architectures, 2006.

P. H. Feiler, D. P. Gluch, and J. J. Hudak, The Architecture Analysis & Design Language (AADL) : An Introduction, 2006.

D. Gajski, SpecC : Specification Language and Methodology, 2000.
DOI : 10.1007/978-1-4615-4515-6

D. Gajski, S. Abdi, A. Gerstlauer, and G. Schirner, Embedded System Desing : Modeling, Synthesis and Verification, 2009.

D. Gajski and R. H. Kuhn, Guest Editors' Introduction: New VLSI Tools, Computer, vol.16, issue.12, pp.11-14, 1983.
DOI : 10.1109/MC.1983.1654264

D. Gajski, F. Vahid, S. Narayan, and J. Gong, System-level Exploration with Spec- Syn, Proceedings of the 35th Annual Design Automation Conference, DAC'98, pp.812-817, 1998.
DOI : 10.1109/dac.1998.724583
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.4788

H. Garavel, F. Lang, R. Mateescu, and W. Serve, CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes, LNCS, vol.56, issue.3, 2011.
DOI : 10.1007/BFb0054166
URL : https://hal.archives-ouvertes.fr/inria-00583776

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP 2011: a toolbox for the construction and analysis of distributed processes, International Journal on Software Tools for Technology Transfer, vol.1, issue.1/2, 2012.
DOI : 10.1007/s10009-012-0244-z
URL : https://hal.archives-ouvertes.fr/hal-00715056

D. Genius, E. Faure, and N. Pouillon, Mapping a Telecommunication Application on a??Multiprocessor System-on-Chip, Algorithm-Architecture Matching for Signal and Image Processing, pp.53-77, 2011.
DOI : 10.1007/978-90-481-9965-5_3
URL : https://hal.archives-ouvertes.fr/hal-01287781

S. Grumbach and T. Milo, An algebra for pomsets, Database Theory ICDT'95, pp.191-207, 1995.
DOI : 10.1007/3-540-58907-4_16

N. Guelfi and B. Ries, SESAME : A Model-Driven Test Selection Process for Safety- Critical Embedded Systems, 2008.

R. K. Gupta, C. N. Coelho, and G. D. Micheli, Synthesis and simulation of digital systems containing interacting hardware and software components, Proceedings of the 29th ACM/IEEE Design Automation Conference, DAC'92, pp.225-230, 1992.

N. Halbwachs, A Synchronous Language at Work: The Story of Lustre, Formal Methods and Models for Co-Design, 2005. MEMOCODE'05. Proceedings. Third ACM and IEEE International Conference on, pp.3-11, 2005.
DOI : 10.1002/9781118459898.ch2
URL : https://hal.archives-ouvertes.fr/hal-00190883

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous dataflow programming language lustre, Proceedings of the IEEE, pp.1305-1320, 1991.

G. Hamon and M. Pouzert, Modular resetting of synchronous data-flow programs, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '00, pp.289-300, 2000.
DOI : 10.1145/351268.351300

G. J. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1997.
DOI : 10.1109/32.588521

D. Hommais, F. Petrot, and I. Auge, A practical tool box for system level communication synthesis, Proceedings of the ninth international symposium on Hardware/software codesign , CODES '01, pp.48-53, 2001.
DOI : 10.1145/371636.371674

Y. Hwang, G. Schirner, and S. Abdi, Automatic Generation of Cycle-Approximate TLMs with Timed RTOS Model Support, Analysis, Architectures and Modelling of Embedded Systems, Third IFIP TC 10 International Embedded Systems Symposium , IESS 2009, pp.66-76, 2009.
DOI : 10.1007/978-1-4615-4515-6

L. Isenegger, L. Jérôme, and W. O. Cesário, Verifying a CoFluent SystemC IP Model from a SystemVerilog UVM Testbench in Mentor Graphics Questa, 2010.

C. Jaber, A. Kanstein, L. Apvrille, A. Baghdadi, P. L. Moenner et al., High-Level System Modeling for Rapid HW/SW Architecture Exploration, 2009 IEEE/IFIP International Symposium on Rapid System Prototyping, pp.88-94, 2009.
DOI : 10.1109/RSP.2009.27

B. Johan and Y. Wang, Timed Automata : Semantics, Algorithms and Tools. Lectures on Concurrency and Petri Nets, pp.87-124, 2004.

D. Knorreck, L. Apvrille, and R. Pacalet, Fast Simulation Techniques for Design Space Exploration, Objects, Components, Models and Patterns 47th International Conference, TOOLS EUROPE-09 Lecture Notes in Business Information Processing, pp.308-327, 2009.
DOI : 10.1109/TC.2006.16

D. Ku and G. D. Micheli, HardwareC -A Language for Hardware Design Version 2.0, 1990.

E. Lee and T. Parks, Dataflow process networks, Proceedings of the IEEE, pp.773-801, 1995.
DOI : 10.1109/5.381846
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.2539

E. A. Lee, Finite State Machines and Modal Models in Ptolemy II, 2009.

H. G. Lee, N. Chang, U. Y. Ogras, and R. Marculescu, On-chip communication architecture exploration, ACM Transactions on Design Automation of Electronic Systems, vol.12, issue.3, 2007.
DOI : 10.1145/1255456.1255460

P. Lieverse, P. V. Wolf, and E. D. Deprettere, A trace transformation technique for communication refinement, CODES'01 : Proceedings of the ninth international symposium on Hardware/software codesign, 2001.

S. Maharaj and J. Bicarregui, On the verification of VDM specification and refinement with PVS, Proceedings 12th IEEE International Conference Automated Software Engineering, pp.157-190, 1997.
DOI : 10.1109/ASE.1997.632849

F. Maraninchi and Y. Rémond, Mode-Automata: a new domain-specific construct for the development of safe critical systems, Science of Computer Programming, vol.46, issue.3, pp.219-254, 2003.
DOI : 10.1016/S0167-6423(02)00093-X

R. Marculescu, Ü. Y. Ogras, and N. H. Zamora, Computation and communication refinement for multiprocessor SoC design, ACM Transactions on Design Automation of Electronic Systems, vol.11, issue.3, pp.564-592, 2006.
DOI : 10.1145/1142980.1142983

R. Mateescu and D. Thivolle, A Model Checking Language for Concurrent Value-Passing Systems, FM 2008 : Formal Methods, pp.148-164, 2008.
DOI : 10.1007/978-3-540-68237-0_12
URL : https://hal.archives-ouvertes.fr/inria-00315312

K. L. Mcmillan, Symbolic Model Checking, 1993.

J. Mikác and P. Caspi, Flush: an example of development by refinements in SCADE/Lustre, International Journal on Software Tools for Technology Transfer, vol.16, issue.1, pp.409-418, 2009.
DOI : 10.1007/s10009-009-0113-6

H. Mokrani and R. Ameur-boulifa, A Refinement Approach to Design and Verification of On-Chip Communication Protocols Journée du Groupe SAFA (Sophia- Antipolis Formal Analysis Group), informal proceeding, 2011.

H. Mokrani, R. Ameur-boulifa, S. Coudert, and E. Encrenaz-tiphène, Communication Refinement for SOC Design Journée du Groupe SAFA (Sophia-Antipolis Formal Analysis Group), informal proceeding, 2010.

H. Mokrani, R. Ameur-boulifa, and E. Encrenaz-tiphene, Assisting Refinement in System-on-Chip Design, Forum on Specification Design Languages, FDL'13, pp.1-6, 2013.
DOI : 10.1007/978-3-319-06317-1_2
URL : https://hal.archives-ouvertes.fr/hal-01216546

H. Mokrani, R. Ameur-boulifa, and E. Encrenaz-tiphene, Assisting Refinement In System-on-Chip Design Models, Methods and Tools for Complex Chip Design, selected contributions from FDL'13, Lecture Notes in Electrical Engineering, p.2014

H. Mokrani, R. Ameur-boulifa, E. Encrenaz-tiphène, and S. Coudert, Approche pour l???int??gration du raffinement formel dans le processus de conception des SoCs, Journal Européen des Systèmes Automatisés (JESA), Special Issue MSR'11, pp.221-236, 2011.
DOI : 10.3166/jesa.45.221-236

S. Nicolas, Systèmes de transitions symboliques et hiérarchiques pour la conception et la validation de modèles B raffinés, 2007.

T. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL -A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science LNCS, vol.2283, 2002.

D. A. Padua and M. J. Wolfe, Advanced compiler optimizations for supercomputers, Communications of the ACM, vol.29, issue.12, pp.1184-1201, 1986.
DOI : 10.1145/7902.7904

P. R. Panda, SystemC, Proceedings of the 14th international symposium on Systems synthesis , ISSS '01, pp.75-80, 2001.
DOI : 10.1145/500001.500018

R. Passerone, L. De-alfaro, T. A. Henzinger, and A. L. Sangiovanni-vincentelli, Convertibility verification and converter synthesis, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design , ICCAD '02, pp.132-139, 2002.
DOI : 10.1145/774572.774592

O. Pell, Verification of FPGA Layout Generators in Higher-Order Logic, Journal of Automated Reasoning, vol.17, issue.4, pp.117-152, 2006.
DOI : 10.1007/s10817-006-9039-9

A. Pimentel, L. Hertzbetger, P. Lieverse, V. D. Wolf, and E. Deprettere, Exploring embedded-systems architectures with Artemis, Computer, vol.34, issue.11, pp.3457-63, 2001.
DOI : 10.1109/2.963445

N. Pontisso and D. Chemouil, TOPCASED Combining Formal Methods with Model-Driven Engineering ASE'06, Automated Software Engineering 21st IEEE/ACM International Conference on, pp.359-360, 2006.

V. R. Pratt, The pomset model of parallel processes: Unifying the temporal and the spatial, Seminar on Concurrency, pp.180-196, 1984.
DOI : 10.1007/3-540-15670-4_9

J. P. Queille and J. Sifakis, A temporal logic to deal with fairness in transition systems, 23rd Annual Symposium on Foundations of Computer Science (sfcs 1982), pp.217-225, 1982.
DOI : 10.1109/SFCS.1982.57

P. Rashinkar, P. Paterson, and L. Singh, System-on-a-chip Verification : Methodology and Techniques, 2000.

E. Rigoni, C. Kavka, A. Turco, G. Palermo, C. Silvano et al., Optimization Algorithms for Design Space Exploration of Embedded Systems, Multi-objective Design Space Exploration of Multiprocessor SoC Architectures, pp.51-74, 2011.
DOI : 10.1007/978-1-4419-8837-9_3

A. W. Roscoe and N. Dathi, The pursuit of deadlock freedom, Information and Computation, vol.75, issue.3, pp.289-327, 1987.
DOI : 10.1016/0890-5401(87)90004-6

A. W. Roscoe, C. A. Hoare, and R. Bird, The Theory and Practice of Concurrency, 1997.

D. Sabatier and P. Lartigue, The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications, Formal Methods (FM'99), pp.348-368, 1999.
DOI : 10.1007/3-540-48119-2_21

F. Schirrmeister and A. Sangiovanni-vincentelli, Virtual component co-designapplying function architecture co-design to automotive applications, Vehicle Electronics Conference Proceedings of the IEEE International, pp.221-226, 2001.

F. B. Schneider and D. Gries, Refinement Calculus : A Systematic Introduction, 1998.

K. Seidel, Case study: Specification and refinement of the PI-Bus, FME'94 : Industrial Benefit of Formal Methods, pp.532-546, 1994.
DOI : 10.1007/3-540-58555-9_114

T. Shanley and D. Anderson, PCI System Architecture, 2006.

D. Shin, S. Abdi, and D. Gajski, Automatic generation of bus functional models from transaction level models, Design Automation : Electronic Design and Solution Fair, pp.756-758, 2004.

W. T. Shiue and C. Chakrabarti, Memory exploration for low power, embedded systems, Proceedings of the 36th ACM/IEEE conference on Design automation conference , DAC '99, pp.140-145, 1999.
DOI : 10.1145/309847.309902

A. Siemens, PI-Bus (Rev. 0.3d) : Draft standard OMI 324, 1994.

G. Smith, The Object-Z Specification Language, 2000.
DOI : 10.1007/978-1-4615-5265-9

O. Tardieu, A deterministic logical semantics for pure Esterel, ACM Transactions on Programming Languages and Systems, vol.29, issue.2, 2007.
DOI : 10.1145/1216374.1216376

F. Vahid and T. Givargis, Embedded System Design : A Unified Hardware/Software Introduction, 2001.

R. Van-glabbeek, The Linear Time ? Branching Time Spectrum I ; The Semantics of Concrete, Sequential Processes, Handbook of Process Algebra, pp.3-99, 2001.

K. S. Wolff, T. Santen, and B. Wolff, A Structure Preserving Encoding of Z in Isabelle/HOL, Theorem Proving in Higher-Order Logics, pp.283-298, 1996.

J. Woodcock and J. Davies, Using Z specification, refinement and proof, 1996.