@. A. Kriouile and W. Serwe, Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip, TACAS, LNCS 9035, pp.708-722, 2015.
DOI : 10.1007/978-3-662-46681-0_62
URL : https://hal.archives-ouvertes.fr/hal-01104747

@. A. Kriouile and W. Serwe, Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip, FMICS, pp.108-122, 2013.
DOI : 10.1007/978-3-642-41010-9_8
URL : https://hal.archives-ouvertes.fr/hal-00858521

@. A. Kriouile and W. Serwe, Analyse formelle du protocole ACE : cohérence de caches des systèmes sur puce In ETR, 9.3. Scientific Publications and Communications 9.3.2 Scientific Communications Invited talk, pp.130-133, 2013.

@. A. Kriouile and W. Serwe, Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip, Cadence Club Formal, 2015.
DOI : 10.1007/978-3-662-46681-0_62
URL : https://hal.archives-ouvertes.fr/hal-01104747

@. A. Kriouile and W. Serwe, Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip, TACAS, part of ETAPS 2015, 2015.
DOI : 10.1007/978-3-662-46681-0_62
URL : https://hal.archives-ouvertes.fr/hal-01104747

@. A. Kriouile and M. Zendri, 20 years of Hardware Verification with CADP, Formal Methods Forum, LAAS laboratory, 2014.

@. A. Kriouile and W. Serwe, Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip, FMICS, 2013.
DOI : 10.1007/978-3-642-41010-9_8
URL : https://hal.archives-ouvertes.fr/hal-00858521

@. A. Kriouile and M. Zendri, Model based test generation for cache coherent Systemson-Chips, Presentations in national seminars: Formal Methods Forum, LAAS laboratory, 2015.

@. A. Kriouile, Formal Methods for Functional Verification of Cache-Coherent SoCs, CONVECS'2015, 2015.

@. A. Kriouile, Model-Based Testing of SoCs: from Theory to Practice, CON- VECS'2014, 2014.

@. A. Kriouile, Introduction of Formal High Level Modeling into SoC Validation: Illustration on ACE compliant Cache Coherence, CONVECS'2013, 2013.

@. A. Kriouile, Formal Modeling and Verification of an ACE Compliant Cache Coherent Interconnect, CONVECS'2012, 2012.

@. A. Kriouile}, Validation of Distributed Systems on-Chip Shared dirty data integrity not ({?Ch:String ?op:String !m1 !l ?s:String where ace_state (s) and (s<>, LIG'2013. A.6

{. Ch, String ?op:String ?m2:Nat !l ?data2:Nat ?"ACE_SC" where (m2<>m1) and (data2<>data1

{. Op, String !m !l ?any of Nat ?any of bool ?any of bool !"FALSE"} . ( ( not({?Ch:String ?op:String !m !l ?s:String}) and ( not{CR ?op:String !m !l, }) )*

{. Ch, String ?op:String !m !l

{. Op, String !m !l ?any of Nat ?any of bool ?any of bool !"TRUE"} . ( ( not({?Ch:String ?op:String !m !l ?s:String}) and ( not{CR ?op:String !m !l, }) )*

{. Ch, String ?op:String !m !l ?ACE_I"} ] false Bibliography [ABG + 00] Yael Abarbanel Focs?automatic generation of simulation checkers from formal specifications, Computer Aided Verification, pp.538-542, 2000.

L. Aceto, W. Fokkink, and C. Verhoef, Structural Operational Semantics, pp.197-292, 2001.

F. David and . Anderson, Continuous-time markov chains, 1991.

[. Arm, CoreLink CCI-400 Cache Coherent Interconnect: Technical Reference Manual revision r1p1, version ARM IHI 0022E, 2012.

M. Ben-ari, A. Pnueli, and Z. Manna, The temporal logic of branching time, Acta Informatica, vol.20, issue.4, pp.207-226, 1983.
DOI : 10.1007/BF01257083

[. Bolognesi and E. Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, vol.14, issue.1, pp.25-59, 1988.
DOI : 10.1016/0169-7552(87)90085-7

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

]. J. Bcl-+-94, E. Burch, D. Clarke, K. Long, D. Mcmillan et al., Symbolic model checking for sequential circuit verification, IEEE Trans. Computer-Aided Design Integration of Circuits, vol.13, pp.401-424, 1994.

R. Jerry, E. M. Burch, . Clarke, L. Kenneth, . Mcmillan et al., Symbolic model checking: 10 20 states and beyond, Bibliography Logic in Computer Science, 1990. LICS'90, Proceedings., Fifth Annual IEEE Symposium on e, pp.428-439, 1990.

V. Beaudenon, E. Encrenaz, and J. Desbarbieux, Design validation of ZCSP with SPIN, Third International Conference on Application of Concurrency to System Design, 2003. Proceedings., pp.102-110, 2003.
DOI : 10.1109/CSD.2003.1207704

D. Benjamin, A. Geist, G. Hartman, R. Mas, and . Smeets, A Study in Coverage-Driven Test Generation, Proceedings of the 36th Design Automation Conference, pp.970-975, 1999.

J. Baier and . Katoen, Principles of model checking, 2008.

[. Blanc, D. Kroening, and N. Sharygina, Scoot: A Tool for the Analysis of SystemC??Models, Tools and Algorithms for the Construction and Analysis of Systems, pp.467-470, 2008.
DOI : 10.1007/978-3-540-78800-3_36

M. [. Clarke, X. Fujita, and . Zhao, Hybrid decision diagrams, International Conference on Computer-Aided Design, ICCAD-95, pp.159-163, 1995.

E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long et al., Verification of the Futurebus+ cache coherence protocol, Formal Methods in System Design, vol.13, issue.2, pp.217-232, 1995.
DOI : 10.1007/BF01383968

H. Cgm-+-96-]-ghassan-chehaibar, L. Garavel, N. Mounier, F. Tawbi, and . Zulian, Specification and verification of the powerscale bus arbitration protocol: An industrial experiment with lotos, Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE/P- STV'96, pp.435-450, 1996.

M. Edmund and . Clarke, Orna Grumberg, and Doron Peled. Model checking, 2000.

[. Coste, H. Hermanns, E. Lantreibecq, and W. Serwe, Towards Performance Prediction of Compositional Models in Industrial GALS Designs, Proceedings of the 21th International Conference on Computer Aided Verification CAV'2009, pp.204-218, 2009.
DOI : 10.1007/978-3-642-02658-4_18
URL : https://hal.archives-ouvertes.fr/inria-00381657

[. Crouzen and F. Lang, Smart Reduction, Proceedings of Fundamental Approaches to Software Engineering FASE'2011, pp.111-126, 2011.
DOI : 10.1007/978-3-642-19811-3_9
URL : https://hal.archives-ouvertes.fr/inria-00572535

M. Chen and P. Mishra, Property Learning Techniques for Efficient Generation of Directed Tests, IEEE Transactions on Computers, vol.60, issue.6, pp.852-864, 2011.
DOI : 10.1109/TC.2011.49

[. Chen, X. Qin, H. Koo, and P. Mishra, System- Level Validation: High-Level Modeling and Directed Test Generation Techniques, 2013.
DOI : 10.1007/978-1-4614-1359-2

R. Cleaveland and S. A. Smolka, Strategic directions in concurrency research, ACM Computing Surveys, vol.28, issue.4, pp.607-625, 1996.
DOI : 10.1145/242223.242252

[. Clarke, M. Talupur, H. Veith, and D. Wang, SAT Based Predicate Abstraction for Hardware Verification, Theory and Applications of Satisfiability Testing, pp.78-92, 2004.
DOI : 10.1007/978-3-540-24605-3_7

[. Chen, Y. Yang, G. Gopalakrishnan, and C. Chou, Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols. Formal Methods in System Design, pp.37-64, 2010.

G. Chehaibar, M. Zidouni, and R. Mateescu, Modeling Multiprocessor Cache Protocol Impact on MPI Performance, 2009 International Conference on Advanced Information Networking and Applications Workshops, pp.1073-1078, 2009.
DOI : 10.1109/WAINA.2009.117
URL : https://hal.archives-ouvertes.fr/inria-00381674

R. Drechsler, C. Chevallaz, F. Fummi, A. J. Hu, R. Morad et al., Future soc verification methodology: Uvm evolution or revolution, Proceedings of the conference on Design European Design and Automation Association, p.372, 2014.

D. L. Dill, A. J. Drexler, A. J. Hu, and C. Yang, Protocol verification as a hardware design aid, Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computers & Processors, pp.522-525, 1992.
DOI : 10.1109/ICCD.1992.276232

G. Dowek, A. Felty, H. Herbelin, G. Huet, and B. Werner, Christine Paulin-Mohring, et al. The coq proof assistant user's guide: Version 5, 1991.

A. Dahan, D. Geist, L. Gluhovsky, D. Pidan, G. Shapir et al., Combining System Level Modeling with Assertion Based Verification, Sixth International Symposium on Quality of Electronic Design (ISQED'05), pp.310-315, 2005.
DOI : 10.1109/ISQED.2005.32

]. D. Dil96 and . Dill, The mur? verification system, Proceedings of the 8th International Conference on Computer-Aided Verification CAV'96, 1996.

G. René, J. De-vries, and . Tretmans, Towards formal test purposes, Formal Approaches to Testing of Software FATES'01, pp.61-76, 2001.

Á. Th, K. L. Eiríksson, and . Mcmillan, Using Formal Verification/- Analysis Methods on the Critical Path in System Design: A Case Study, Proceedings of the 7th International Conference on Computer Aided Verification CAV, pp.367-380, 1995.

J. Fernandez, C. Jard, T. Jéron, and C. Viho, Using on-the-fly verification techniques for the generation of test suites, Computer Aided Verification, pp.348-359, 1996.
DOI : 10.1007/3-540-61474-5_82
URL : https://hal.archives-ouvertes.fr/inria-00073711

S. Foroutan, Y. Thonnart, R. Hersemeule, and A. Jerraya, A Markov chain based method for NoC end-to-end latency evaluation, 2010 IEEE International Symposium on Parallel & Distributed Processing, Workshops and Phd Forum (IPDPSW), pp.1-8, 2010.
DOI : 10.1109/IPDPSW.2010.5470788

C. [. Gargantini and . Heitmeyer, Using model checking to generate tests from requirements specifications, ACM SIGSOFT Software Engineering Notes, vol.24, issue.6, pp.146-162, 1999.
DOI : 10.1145/318774.318939

H. Garavel and H. Hermanns, On Combining Functional Verification and Performance Evaluation Using CADP, Proceedings of the 11th International Symposium of Formal Methods Europe FME, pp.410-429, 2002.
DOI : 10.1007/3-540-45614-7_23
URL : https://hal.archives-ouvertes.fr/inria-00072096

H. Garavel, C. Helmstetter, O. Ponsini, and W. Serwe, Verification of an industrial SystemC/TLM model using LOTOS and CADP, 2009 7th IEEE/ACM International Conference on Formal Methods and Models for Co-Design, 2009.
DOI : 10.1109/MEMCOD.2009.5185377
URL : https://hal.archives-ouvertes.fr/inria-00408283

H. Garavel and F. Lang, SVL: A Scripting Language for Compositional Verification, Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2001, pp.377-392, 2001.
DOI : 10.1007/0-306-47003-9_24
URL : https://hal.archives-ouvertes.fr/inria-00072396

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, Cadp 2011: A toolbox for the construction and analysis of distributed processes. Software Tools for Technology Transfer, pp.89-107, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00715056

H. Garavel, R. Mateescu, and . Seq, open: A tool for efficient tracebased verification, Proceedings of the 11th International SPIN Workshop on Model Checking of Software SPIN, pp.150-155, 2004.

M. Gordon, HOL-a machine oriented formulation of higher order logic. Citeseer, 2001.

H. Garavel, C. Viho, and M. Zendri, System design of a cc-numa multiprocessor architecture using formal specification, model-checking, cosimulation , and test generation, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00072597

H. Garavel, C. Viho, and M. Zendri, System design of a ccnuma multiprocessor architecture using formal specification, model-checking, Bibliography co-simulation, and test generation, International Journal on Software Tools for Technology Transfer, vol.3, issue.3, pp.314-331, 2001.

X. Michel, . Goemans, P. David, and . Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, Journal of the ACM (JACM), vol.42, issue.6, pp.1115-1145, 1995.

H. Hermanns, Interactive Markov chains: and the quest for quantified quality, 2002.

J. Gerard and . Holzmann, State compression in spin: Recursive indexing and compression training runs, Proceedings of SPIN97 the 3rd SPIN Workshop, 1997.

[. Iso, Osi 8807-lotos: a formal description technique based on the temporal ordering of observational behaviour, International standard, ISO, 1989.

C. Jard and T. Jéron, TGV: theory, principles and algorithms, International Journal on Software Tools for Technology Transfer, vol.17, issue.4, pp.297-315, 2005.
DOI : 10.1007/s10009-004-0153-x

P. [. Jéron and . Morel, Test Generation Derived from Model-Checking, Proceedings of the Conference on Computer-Aided Verification CAV'99, pp.108-122, 1999.
DOI : 10.1007/3-540-48683-6_12

B. Robert, . Jones, W. John, C. Leary, . Seger et al., Practical formal verification in microprocessor design, IEEE Design & Test of Computers, vol.18, issue.4, pp.16-25, 2001.

[. Jackson and J. Wing, Lightweight Formal Methods, IEEE Computer, vol.29, issue.1, pp.21-22, 1996.
DOI : 10.1007/3-540-45251-6_1

D. Kästner, TDL: A Hardware Description Language for Retargetable Postpass Optimizations and Analyses, Generative Programming and Component Engineering, pp.18-36, 2003.
DOI : 10.1007/978-3-540-39815-8_2

C. Kern and M. R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems, vol.4, issue.2, pp.123-193, 1999.
DOI : 10.1145/307988.307989

K. Hemangee, P. Kapoor, M. Kanakala, S. Verma, and . Das, Design and formal verification of a hierarchical cache coherence protocol for NoC based multiprocessors, The Journal of Supercomputing, 2013.

M. Kaufmann and J. Strother-moore, ACL2: an industrial strength version of Nqthm, Proceedings of 11th Annual Conference on Computer Assurance. COMPASS '96, pp.23-34, 1996.
DOI : 10.1109/CMPASS.1996.507872

J. Krimm and L. Mounier, Compositional state space generation from Lotos programs, Tools and Algorithms for the Construction and Analysis of Systems TACAS'1997, pp.239-258, 1997.
DOI : 10.1007/BFb0035392

H. Koo, P. Mishra, J. Bhadra, and M. Abadir, Directed Micro-architectural Test Generation for an Industrial Processor: A Case Study, Seventh International Workshop on Microprocessor Test and Verification (MTV'06), pp.33-36, 2006.
DOI : 10.1109/MTV.2006.10

M. Kwiatkowska, G. Norman, and R. Segala, Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM?, Computer Aided Verification, pp.194-206, 2001.
DOI : 10.1007/3-540-44585-4_17

D. Kozen, Results on the propositional µ-calculus. Theoretical computer science, pp.333-354, 1983.

[. Kriouile and W. Serwe, Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip, Proceedings of the 18th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2013, pp.108-122, 2013.
DOI : 10.1007/978-3-642-41010-9_8
URL : https://hal.archives-ouvertes.fr/hal-00858521

A. Kriouile and W. Serwe, Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip, 21th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2015, pp.708-722, 2015.
DOI : 10.1007/978-3-662-46681-0_62
URL : https://hal.archives-ouvertes.fr/hal-01104747

H. Kahlouche, C. Viho, and M. Zendri, An industrial experiment in automatic generation of executable test suites for a cache coherency protocol, Testing of Communicating Systems, pp.211-226, 1998.
DOI : 10.1007/978-0-387-35381-4_13

[. Kyung, Current status and challenges of soc verification for embedded systems market, IEEE International SOC Conferenceg. IEEE, 2003.

G. Lenzi, The modal mu-calculus: a survey, TASK Quarterly, 2005.

S. Liao, G. Martin, S. Swan, and T. Grötker, System Design with SystemC, 2002.

E. Lantreibecq and W. Serwe, Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit Using CADP, Proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems FMICS 2011, pp.180-195, 2011.
DOI : 10.1007/978-3-642-24431-5_14
URL : https://hal.archives-ouvertes.fr/hal-00642029

E. Lantreibecq and W. Serwe, Formal analysis of a hardware dynamic task dispatcher with CADP, Science of Computer Programming, vol.80, pp.130-149, 2014.
DOI : 10.1016/j.scico.2013.01.003
URL : https://hal.archives-ouvertes.fr/hal-00782069

R. Mateescu, On-the-Fly Verification using CADP, Thomas Arts and Wan Fokkink Proceedings of the 8th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2003, 2003.
DOI : 10.1016/S1571-0661(04)80826-0

[. Mishra and M. Chen, Efficient Techniques for Directed Test Generation Using Incremental Satisfiability, 2009 22nd International Conference on VLSI Design, pp.65-70, 2009.
DOI : 10.1109/VLSI.Design.2009.72

L. Kenneth and . Mcmillan, Symbolic model checking, 1993.

L. Kenneth and . Mcmillan, The SMV language, 1999.

L. Kenneth and . Mcmillan, A methodology for hardware verification using compositional model checking, Science of Computer Programming, vol.37, issue.1, pp.279-309, 2000.

F. Tom and . Melham, Higher order logic and hardware verification, 2009.

M. K. Milo, M. D. Martin, D. J. Hill, and . Sorin, Why On-Chip Cache Coherence Is Here to Stay, Communications of the ACM, vol.55, issue.7, pp.78-89, 2012.

L. Kenneth and S. Mcmillan, Formal Verification of the Encore Gigamax cache consistency protocol, Proceedings of the International Symposium on Shared Memory Multiprocessors, pp.242-251, 1991.

A. Deepak, . Mathaikutty, K. Sandeep, . Shukla, V. Sreekumar et al., Design fault directed test generation for microprocessor validation, Design, Automation & Test in Europe Conference & Exhibition DATE'07, pp.1-6, 2007.

[. Mateescu and D. Thivolle, A Model Checking Language for Concurrent Value-Passing Systems, Proceedings of the 15th International Symposium on Formal Methods FM'08, pp.148-164, 2008.
DOI : 10.1007/978-3-540-68237-0_12
URL : https://hal.archives-ouvertes.fr/inria-00315312

[. Owre, M. John, N. Rushby, and . Shankar, PVS: A prototype verification system, Automated Deduction-CADE-11, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

[. Park, Concurrency and automata on infinite sequences, Theoretical Computer Science, 1981.
DOI : 10.1007/BFb0017309

C. Lawrence and . Paulson, Isabelle: A generic theorem prover, 1994.

F. Pong and M. Dubois, Verification techniques for cache coherence protocols, ACM Computing Surveys, vol.29, issue.1, pp.82-126, 1997.
DOI : 10.1145/248621.248624

[. Greenhalgh, Big. little processing with arm cortex TM -a15 & cortex-a7, 2011.

L. Pierre, Outils de démonstration automatique et preuve de circuits électroniques. Forum Méthodes Formelles: Preuve de modèle, 2014.

F. Pong, A. Nowatzyk, G. Aybay, and M. Dubois, Verifying distributed directory-based cache coherence protocols: S3.mp, a case study, Proceedings of the 1st International Conference on Parallel Processing EURO-PAR'95, pp.287-300, 1995.
DOI : 10.1007/BFb0020472

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977.
DOI : 10.1109/SFCS.1977.32

K. Dhiraj and . Pradhan, Application of galois fields to logic synthesis, Industrial and Information Systems ICIIS 2008. IEEE Region 10 and the Third international Conference on, pp.1-1, 2008.

X. Qin and P. Mishra, Efficient directed test generation for validation of multicore architectures, 2011 12th International Symposium on Quality Electronic Design, pp.276-283, 2011.
DOI : 10.1109/ISQED.2011.5770737

A. Roychoudhury, T. Mitra, and S. Karri, Using formal techniques to debug the amba system-on-chip bus protocol Automatic Verification of the SCI Cache Coherence Protocol, Design, Automation and Test in Europe Conference and Exhibition Correct Hardware Design and Verification Methods, pp.828-833, 1995.

A. Slobodová, J. Davis, S. Swords, W. Hunt, and J. , A Flexible Formal Verification Framework for Industrial Scale Verification, Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign MEMOCODE 2011, pp.89-97, 2011.

. Selman, J. Hector, . Levesque, G. David, and . Mitchell, A new method for solving hard satisfiability problems, AAAI, pp.440-446, 1992.

G. Salaun, W. Serwe, Y. Thonnart, and P. Vivet, Formal Verification of CHP Specifications with CADP Illustration on an Asynchronous Network-on-Chip, 13th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'07), pp.73-82, 2007.
DOI : 10.1109/ASYNC.2007.18
URL : https://hal.archives-ouvertes.fr/inria-00200450

A. Stevens, Introduction to AMBA 4 ACE. ARM whitepaper, 2011.

S. Sutherland, Modeling with systemverilog in a synopsys synthesis design flow using leda, vcs, design compiler and formality. SNUG Europe, 2006.

[. Swan, SystemC transaction level models and RTL verification, Proceedings of the 43rd annual conference on Design automation , DAC '06, pp.90-92, 2006.
DOI : 10.1145/1146909.1146937

W. Shen, Y. Wei, B. Chen, Q. Chen, and . Guo, Coverage Directed Test Generation: Godson Experience, 2008 17th Asian Test Symposium, pp.321-326, 2008.
DOI : 10.1109/ATS.2008.42

[. Thompson, Verifying Cache Coherency Protocols with Verification IP. Synopsis, 2012.

J. Tretmans, Test generation with inputs, outputs and repetitive quiescence. Software?Concepts and Tools, 1996.

J. Tretmans, Testing Concurrent Systems: A Formal Approach, CON- CUR'99 Concurrency Theory, pp.46-65, 1999.
DOI : 10.1007/3-540-48320-9_6

[. Vizel, O. Grumberg, and S. Shoham, Lazy abstraction and sat-based reachability in hardware model checking, Formal Methods in Computer-Aided Design (FMCAD), 2012, pp.173-181, 2012.

R. Jan, V. Glabbeek, and W. P. Weijland, Refinement in branching time semantics, Centrum voor Wiskunde en Informatica, Computer science, 1989.

J. Rob, W. Van-glabbeek, and . Peter-weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM (JACM), vol.43, issue.3, pp.555-600, 1996.

M. Weiglhofer, K. Bernhard, F. Aichernig, and . Wotawa, Fault-based conformance testing in practice, Int. J. Software and Informatics, vol.3, issue.2-3, pp.375-411, 2009.

P. Wodey, G. Camarroque, F. Baray, R. Hersemeule, and J. Cousin, LOTOS code generation for model checking of STBus based SoC: the STBus interconnection, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2003. MEMOCODE '03. Proceedings., 2003.
DOI : 10.1109/MEMCOD.2003.1210105

J. Yuan, C. Pixley, A. Aziz, and K. Albin, A framework for constrained functional verification, International Conference on Computer Aided Design, pp.142-145, 2003.

W. Zhang, J. Serwe, T. Wu, H. Yoneda, C. Zheng et al., Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip, Proceedings of the 18th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2014, pp.48-62, 2014.
DOI : 10.1007/978-3-319-10702-8_4
URL : https://hal.archives-ouvertes.fr/hal-01064829