M. Abadi and L. Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems, vol.15, issue.1, pp.73-132, 1993.
DOI : 10.1145/151646.151649

M. Abadi and L. Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems, vol.17, issue.3, pp.507-534, 1995.
DOI : 10.1145/203095.201069

M. Abadi, L. Lamport, and P. Wolper, Realizable and unrealizable specifications of reactive systems, Lecture Notes in Computer Science, vol.372, pp.1-17, 1989.
DOI : 10.1007/BFb0035748

Y. Abarbanel, I. Beer, L. Gluhovsky, S. Keidar, and Y. Wolfsthal, FoCs ??? Automatic Generation of Simulation Checkers from Formal Specifications, Computer Aided Verification, pp.538-542, 2000.
DOI : 10.1007/10722167_40

B. , T. Adler, L. Luca-de-alfaro, M. Dias-da-silva, A. Faella et al., Ticc: A Tool for Interface Compatibility and Composition, Proc. of the 18th International Conference on Computer Aided Verification (CAV'06), pp.59-62, 2006.

L. De, A. , and T. A. Henzinger, Interface-based design, Engineering Theories of Software Intensive Systems, proceedings of the Marktoberdorf Summer School. Kluwer, 2004.

R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

R. Alur, L. Fix, and T. A. Henzinger, A determinizable class of timed automata, Lecture Notes in Computer Science, vol.818, pp.1-13, 1994.
DOI : 10.1007/3-540-58179-0_39

R. Alur, L. Fix, and T. A. Henzinger, Event-clock automata: a determinizable class of timed automata, Theoretical Computer Science, vol.211, issue.1-2, pp.253-273, 1999.
DOI : 10.1016/S0304-3975(97)00173-4

R. Alur, T. A. Henzinger, and O. Kupferman, Alternating-time temporal logic, Journal of the ACM, vol.49, issue.5, pp.672-713, 2002.
DOI : 10.1145/585265.585270

R. Alur, T. A. Henzinger, O. Kupferman, and M. Y. Vardi, Alternating refinement relations, Proc. of the 9th International Conference on Concurrency Theory (CONCUR'98), pp.163-178, 1998.
DOI : 10.1007/BFb0055622

A. Antonik, M. Huth, K. G. Larsen, U. Nyman, and A. Wasowski, 20 Years of Modal and Mixed Specifications, Bulletin of European Association of Theoretical Computer Science, vol.1, issue.94, 2008.

A. Antonik, M. Huth, K. G. Larsen, U. Nyman, and A. Wasowski, Complexity of Decision Problems for Mixed and Modal Specifications, FoSSaCS, pp.112-126, 2008.
DOI : 10.1007/978-3-540-78499-9_9

C. Baier and J. Katoen, Principles of Model Checking, 2008.

F. Balarin and R. Passerone, Functional Verification Methodology Based on Formal Interface Specification and Transactor Generation, Proceedings of the Design Automation & Test in Europe Conference, pp.1013-1018, 2006.
DOI : 10.1109/DATE.2006.243899

F. Balarin and R. Passerone, Specification, Synthesis, and Simulation of Transactor Processes, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.26, issue.10, pp.1749-1762, 2007.
DOI : 10.1109/TCAD.2007.895792

F. Balarin, R. Passerone, A. Pinto, and A. L. Sangiovanni-vincentelli, A formal approach to system level design: metamodels and unified design environments, Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE '05., pp.155-163, 2005.
DOI : 10.1109/MEMCOD.2005.1487909

K. Balasubramanian, A. Gokhale, G. Karsai, J. Sztipanovits, and S. Neema, Developing Applications Using Model-Driven Design Environments, Computer, vol.39, issue.2, pp.33-40, 2006.
DOI : 10.1109/MC.2006.54

S. Sebastian, A. Bauer, R. David, K. G. Hennicker, A. Larsen et al., Moving from specifications to contracts in component-based design, Lecture Notes in Computer Science, vol.7212, pp.43-58

S. Sebastian, U. Bauer, L. Fahrenberg, K. G. Juhl, A. Larsen et al., Weighted modal transition systems, Formal Methods in System Design, vol.42, issue.2, pp.193-220, 2013.

S. Sebastian, L. Bauer, K. G. Juhl, A. Larsen, J. Legay et al., Extending modal transition systems with structured labels, Mathematical Structures in Computer Science, vol.22, issue.4, pp.581-617, 2012.

S. Sebastian, P. Bauer, A. Mayer, R. Schroeder, and . Hennicker, On Weak Modal Compatibility, Refinement, and the MIO Workbench, Proc. of 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), pp.175-189, 2010.

N. Benes, J. Kretínsk´kretínsk´y, K. G. Larsen, and J. Srba, Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete, Lecture Notes in Computer Science, vol.5684, pp.112-126, 2009.
DOI : 10.1007/978-3-642-03466-4_7

N. Benes, J. Kretínsk´kretínsk´y, K. G. Larsen, and J. Srba, On determinism in modal transition systems, Theoretical Computer Science, vol.410, issue.41, pp.4026-4043, 2009.
DOI : 10.1016/j.tcs.2009.06.009

B. Caillaud and J. Raclet, Ensuring Reachability by Design, Int. Colloquium on Theoretical Aspects of Computing, 2012.
DOI : 10.1007/978-3-642-32943-2_17

URL : https://hal.archives-ouvertes.fr/hal-00766735

A. Benveniste and G. Berry, The synchronous approach to reactive and real-time systems, Proceedings of the IEEE, vol.79, issue.9, pp.1270-1282, 1991.
DOI : 10.1109/5.97297

URL : https://hal.archives-ouvertes.fr/inria-00075115

A. Benveniste, B. Caillaud, L. P. Carloni, and A. L. Sangiovanni-vincentelli, Tag machines, Proceedings of the 5th ACM international conference on Embedded software , EMSOFT '05, pp.255-263, 2005.
DOI : 10.1145/1086228.1086276

A. Benveniste, B. Caillaud, A. Ferrari, L. Mangeruca, R. Passerone et al., Multiple Viewpoint Contract-Based Specification and Design, Proceedings of the Software Technology Concertation on Formal Methods for Components and Objects, FMCO'07, pp.200-225, 2008.
DOI : 10.1109/43.736561

A. Benveniste, B. Caillaud, D. Nickovic, R. Passerone, J. Raclet et al., Contracts for System Design: Methodology and Application cases, 2015.

A. Benveniste, B. Caillaud, and J. Raclet, Application of interface theories to the separate compilation of synchronous programs, 2012 IEEE 51st IEEE Conference on Decision and Control (CDC), pp.7252-7258, 2012.
DOI : 10.1109/CDC.2012.6426437

URL : https://hal.archives-ouvertes.fr/hal-00721049

A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. L. Guernic et al., The synchronous languages 12 years later, Proceedings of the IEEE, pp.64-83, 2003.
DOI : 10.1109/JPROC.2002.805826

A. Benveniste, D. Nickovic, and T. Henzinger, Compositional Contract Abstraction for System Design, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00938854

L. Benvenuti, A. Ferrari, L. Mangeruca, E. Mazzi, R. Passerone et al., A contract-based formalism for the specification of heterogeneous systems, 2008 Forum on Specification, Verification and Design Languages, pp.142-147, 2008.
DOI : 10.1109/FDL.2008.4641436

G. Berry, The effectiveness of synchronous languages for the development of safety-critical systems, 2003.

N. Bertrand, A. Legay, S. Pinchinat, and J. Raclet, A Compositional Approach on Modal Specifications for Timed Systems, Proc. of the 11th International Conference on Formal Engineering Methods (ICFEM'09), pp.679-697, 2009.
DOI : 10.1007/978-3-642-10373-5_35

URL : https://hal.archives-ouvertes.fr/inria-00418855

N. Bertrand, A. Legay, S. Pinchinat, and J. Raclet, Modal event-clock specifications for timed component-based design, Science of Computer Programming, vol.77, issue.12, 2011.
DOI : 10.1016/j.scico.2011.01.007

URL : https://hal.archives-ouvertes.fr/hal-00752449

N. Bertrand, A. Legay, S. Pinchinat, and J. Raclet, Modal event-clock specifications for timed component-based design, Science of Computer Programming, vol.77, issue.12, 2012.
DOI : 10.1016/j.scico.2011.01.007

URL : https://hal.archives-ouvertes.fr/hal-00752449

N. Bertrand, S. Pinchinat, and J. Raclet, Refinement and Consistency of Timed Modal Specifications, Proc. of the 3rd International Conference on Language and Automata Theory and Applications (LATA'09), pp.152-163, 2009.
DOI : 10.1007/3-540-56922-7_21

URL : https://hal.archives-ouvertes.fr/inria-00424283

A. Beugnard, J. Jézéquel, and N. Plouzeau, Making components contract aware, Computer, vol.32, issue.7, pp.38-45, 1999.
DOI : 10.1109/2.774917

D. Beyer, A. Chakrabarti, and T. A. Henzinger, Web service interfaces, Proceedings of the 14th international conference on World Wide Web , WWW '05, pp.148-159, 2005.
DOI : 10.1145/1060745.1060770

P. Bhaduri and S. Ramesh, Interface synthesis and protocol conversion, Formal Aspects of Computing, vol.32, issue.5, pp.205-224, 2008.
DOI : 10.1007/s00165-007-0045-4

P. Bhaduri and I. Stierand, A proposal for real-time interfaces in SPEEDS, 2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010), pp.441-446, 2010.
DOI : 10.1109/DATE.2010.5457163

S. Bliudze and J. Sifakis, The Algebra of Connectors—Structuring Interaction in BIP, IEEE Transactions on Computers, vol.57, issue.10, pp.1315-1330, 2008.
DOI : 10.1109/TC.2008.26

R. Bloem and B. Jobstmann, Manual for property-based synthesis tool, 2006.

R. Bloem, A. Cimatti, K. Greimel, G. Hofferek, R. Könighofer et al., RATSY ??? A New Requirements Analysis Tool with Synthesis, Lecture Notes in Computer Science, vol.6174, pp.425-429, 2010.
DOI : 10.1007/978-3-642-14295-6_37

G. Booch, J. Rumbaugh, and I. Jacobson, Unified Modeling Language User Guide, The, 2005.

A. Bouali, . Xeve, . Verification, and . Environment, Xeve, an Esterel verification environment, Lecture Notes in Computer Science, vol.1427, pp.500-504, 1998.
DOI : 10.1007/BFb0028770

URL : https://hal.archives-ouvertes.fr/inria-00069957

G. Boudol and K. Larsen, Graphical versus logical specifications, Theoretical Computer Science, vol.106, issue.1, pp.3-20, 1992.
DOI : 10.1016/0304-3975(92)90276-L

URL : https://hal.archives-ouvertes.fr/inria-00075455

F. Bujtor, S. Fendrich, G. Lüttgen, and W. Vogler, Nondeterministic modal interfaces, 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015, pp.152-163, 2015.

F. Bujtor and W. Vogler, Error-pruning in interface automata, 40th International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2014, pp.162-173, 2014.

F. Bujtor and W. Vogler, Failure semantics for modal transition systems, 14th International Conference on Application of Concurrency to System Design , ACSD 2014, pp.42-51, 2014.

J. R. Burch, Trace Algebra for Automatic Verification of Real-Time Concurrent Systems, 1992.

J. R. Burch, R. Passerone, and A. L. Sangiovanni-vincentelli, Overcoming heterophobia: modeling concurrency in heterogeneous systems, Proceedings Second International Conference on Application of Concurrency to System Design, pp.13-32, 2001.
DOI : 10.1109/CSD.2001.981761

B. Caillaud and . Mica, A Modal Interface Compositional Analysis Library, 2011.

B. Caillaud, B. Delahaye, K. G. Larsen, A. Legay, A. Mikkel-larsen-pedersen et al., Compositional Design Methodology with Constraint Markov Chains, 2010 Seventh International Conference on the Quantitative Evaluation of Systems, 2010.
DOI : 10.1109/QEST.2010.23

URL : https://hal.archives-ouvertes.fr/inria-00591578

D. Cancila and R. Passerone, Functional and structural properties in the Model-Driven Engineering approach, 2008 IEEE International Conference on Emerging Technologies and Factory Automation, 2008.
DOI : 10.1109/ETFA.2008.4638491

D. Cancila, R. Passerone, T. Vardanega, and M. Panunzio, Toward Correctness in the Specification and Handling of Non-Functional Attributes of High-Integrity Real-Time Embedded Systems, IEEE Transactions on Industrial Informatics, vol.6, issue.2, pp.181-194, 2010.
DOI : 10.1109/TII.2010.2043741

K. Cerans, J. Chr, K. Godskesen, and . Larsen, Timed Modal Specification ???Theory and Tools, BRICS Report Series, vol.4, issue.11, pp.253-267, 1993.
DOI : 10.7146/brics.v4i11.18802

P. Cern´ycern´y, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, Interface Simulation Distances, Electronic Proceedings in Theoretical Computer Science, vol.96, pp.29-42, 2012.
DOI : 10.4204/EPTCS.96.3

A. Chakrabarti, A Framework for Compositional Design and Analysis of Systems, 2007.

A. Chakrabarti, T. A. Luca-de-alfaro, M. Henzinger, F. Y. Jurdzinski, and . Mang, Interface Compatibility Checking for Software Modules, CAV, pp.428-441, 2002.
DOI : 10.1007/3-540-45657-0_35

A. Chakrabarti, T. A. Luca-de-alfaro, F. Y. Henzinger, and . Mang, Synchronous and Bidirectional Component Interfaces, Proc. of the 14th International Conference on Computer Aided Verification, pp.414-427, 2002.
DOI : 10.1007/3-540-45657-0_34

A. Chakrabarti, T. A. Luca-de-alfaro, M. Henzinger, and . Stoelinga, Resource Interfaces, Lecture Notes in Computer Science, vol.2855, pp.117-133
DOI : 10.1007/978-3-540-45212-6_9

Y. Edward, Z. Chang, A. Manna, and . Pnueli, Characterization of temporal property classes, Lecture Notes in Computer Science, vol.623, pp.474-486, 1992.

T. Chen, C. Chilton, B. Jonsson, and M. Z. Kwiatkowska, A Compositional Specification Theory for Component Behaviours, Lecture Notes in Computer Science, vol.7211, pp.148-168, 2012.
DOI : 10.1007/978-3-642-28869-2_8

URL : https://hal.archives-ouvertes.fr/hal-00665599

C. Chilton, B. Jonsson, and M. Kwiatkowska, An algebraic theory of interface automata, Theoretical Computer Science, vol.549, pp.146-174, 2014.
DOI : 10.1016/j.tcs.2014.07.018

C. Chilton, B. Jonsson, and M. Z. Kwiatkowska, Compositional assume???guarantee reasoning for input/output component theories, Science of Computer Programming, vol.91, pp.115-137, 2014.
DOI : 10.1016/j.scico.2013.12.010

C. Chilton, M. Z. Kwiatkowska, and X. Wang, Revisiting Timed Specification Theories: A Linear-Time Perspective, Lecture Notes in Computer Science, vol.7595, pp.75-90, 2012.
DOI : 10.1007/978-3-642-33365-1_7

URL : https://hal.archives-ouvertes.fr/hal-00739584

E. Clarke, O. Grumberg, and D. Peled, Model Checking, 1999.

E. M. Clarke, D. E. Long, and K. L. Mcmillan, Compositional model checking, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.353-362, 1989.
DOI : 10.1109/LICS.1989.39190

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/hal-01108790

P. Cousot and R. Cousot, Abstract interpretation and application to logic programs, The Journal of Logic Programming, vol.13, issue.2-3, pp.103-179, 1992.
DOI : 10.1016/0743-1066(92)90030-7

P. Cousot and R. Cousot, Abstract Interpretation Frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992.
DOI : 10.1093/logcom/2.4.511

P. Daca, T. Henzinger, W. Krenn, and D. Nickovic, Compositional Specifications for ioco Testing, 2014 IEEE Seventh International Conference on Software Testing, Verification and Validation, 2014.
DOI : 10.1109/ICST.2014.50

W. Damm, E. Thaden, I. Stierand, T. Peikenkamp, and H. Hungar, Using contract-based component specifications for virtual integration testing and architecture design, 2011 Design, Automation & Test in Europe, 2011.
DOI : 10.1109/DATE.2011.5763167

W. Damm and D. Harel, LSCs: Breathing life into message sequence charts, Formal Methods in System Design, vol.19, issue.1, pp.45-80, 2001.
DOI : 10.1023/A:1011227529550

W. Damm, A. Votintseva, A. Metzner, B. Josko, T. Peikenkamp et al., Boosting reuse of embedded automotive applications through rich components, Proceedings of FIT 2005 -Foundations of Interface Technologies, 2005.

A. Davare, D. Densmore, L. Guo, R. Passerone, A. L. Sangiovanni-vincentelli et al., II, ACM Transactions on Embedded Computing Systems, vol.12, issue.1s, pp.1-4931, 2013.
DOI : 10.1145/2435227.2435245

A. David, K. G. Larsen, A. Legay, U. Nyman, and A. Wasowski, Timed I/O automata, Proceedings of the 13th ACM international conference on Hybrid systems: computation and control, HSCC '10, pp.91-100, 2010.
DOI : 10.1145/1755952.1755967

A. David, K. G. Larsen, A. Legay, U. Nyman, and A. Wasowski, ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems, Proc. of the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA'10), pp.365-370, 2010.
DOI : 10.1007/978-3-642-15643-4_29

A. Luca-de, Game Models for Open Systems In Verification: Theory and Practice, Lecture Notes in Computer Science, vol.2772, pp.269-289

L. Luca-de-alfaro, M. Dias-da-silva, A. Faella, P. Legay, M. Roy et al., Sociable Interfaces, Proc. of the 5th International Workshop on Frontiers of Combining Systems (FroCos'05), pp.81-105, 2005.
DOI : 10.1007/11559306_5

L. De, A. , and T. A. Henzinger, Interface automata, Proc. of the 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE'01), pp.109-120, 2001.

L. De, A. , and T. A. Henzinger, Interface theories for componentbased design, Lecture Notes in Computer Science, vol.2211, pp.148-165

T. A. Luca-de-alfaro, M. Henzinger, and . Stoelinga, Timed Interfaces, Proc. of the 2nd International Workshop on Embedded Software (EM- SOFT'02), volume 2491 of Lecture Notes in Computer Science, pp.108-122
DOI : 10.1007/3-540-45828-X_9

B. Delahaye, Modular Specification and Compositional Analysis of Stochastic Systems, 2010.
URL : https://hal.archives-ouvertes.fr/tel-00591609

B. Beno??tbeno??t-delahaye, A. Caillaud, and . Legay, Probabilistic contracts : A compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects. Formal Methods in System Design, 2011.

U. Beno??tbeno??t-delahaye, T. A. Fahrenberg, A. Henzinger, D. Legay, and . Nickovic, Synchronous Interface Theories and Time Triggered Scheduling, Lecture Notes in Computer Science, vol.7273, pp.203-218, 2012.
DOI : 10.1007/978-3-642-30793-5_13

J. Beno??tbeno??t-delahaye, K. G. Katoen, A. Larsen, M. L. Legay, F. Pedersen et al., Abstract Probabilistic Automata, Lecture Notes in Computer Science, vol.2, issue.1-2, pp.324-339, 2011.
DOI : 10.1007/11817949_5

K. G. Beno??tbeno??t-delahaye, A. Larsen, M. L. Legay, A. Pedersen, and . Wasowski, Consistency and refinement for interval markov chains, J. Log

D. Densmore, R. Passerone, and A. L. Sangiovanni-vincentelli, 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

L. David and . Dill, Trace Theory for Automatic Hierarchical Verification of Speed- Independent Circuits, ACM Distinguished Dissertations, 1989.

D. Nicolás, D. Ippolito, M. Fischbein, S. Chechik, and . Uchitel, MTSA: The Modal Transition System Analyser, Proc. of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE'08), pp.475-476, 2008.

L. Doyen, T. A. Henzinger, B. Jobstmann, and T. Petrov, Interface theories with component reuse, Proceedings of the 7th ACM international conference on Embedded software, EMSOFT '08, pp.79-88, 2008.
DOI : 10.1145/1450058.1450070

D. Potop-butucaru, S. Edwards, and G. Berry, Compiling Esterel, 2007.

C. Eisner, R. Psl, and . Verification, PSL for Runtime Verification: Theory and Practice, Lecture Notes in Computer Science, vol.4839, pp.1-8, 2007.
DOI : 10.1007/978-3-540-77395-5_1

C. Eisner, D. Fisman, J. Havlicek, M. J. Gordon, A. Mcisaac et al., Formal Syntax and Semantics of PSL -Appendix B of Accellera LRM, 2003.

C. Eisner, D. Fisman, J. Havlicek, Y. Lustig, A. Mcisaac et al., Reasoning with Temporal Logic on Truncated Paths, Lecture Notes in Computer Science, vol.2725, pp.27-39, 2003.
DOI : 10.1007/978-3-540-45069-6_3

J. Eker, J. W. Janneck, E. A. Lee, J. Liu, X. Liu et al., Taming heterogeneity - the Ptolemy approach, Proc. of the IEEE, pp.127-144, 2003.
DOI : 10.1109/JPROC.2002.805829

O. Ferrante, R. Passerone, A. Ferrari, L. Mangeruca, and C. Sofronis, BCL: A compositional contract language for embedded systems, Proceedings of the 2014 IEEE Emerging Technology and Factory Automation (ETFA), 2014.
DOI : 10.1109/ETFA.2014.7005353

O. Ferrante, R. Passerone, A. Ferrari, L. Mangeruca, C. Sofronis et al., Monitor-based run-time contract verification of distributed systems, Proceedings of the 9th IEEE International Symposium on Industrial Embedded Systems (SIES 2014), 2014.
DOI : 10.1109/SIES.2014.7087332

G. Feuillade, Modal specifications are a syntactic fragment of the Mu-calculus, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000139

D. Fischbein and S. Uchitel, On correct and complete strong merging of partial behaviour models, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, SIGSOFT '08/FSE-16, pp.297-307, 2008.
DOI : 10.1145/1453101.1453144

F. Boussinot, R. De, and S. , The ESTEREL language, Proceedings of the IEEE, pp.1293-1304, 1991.
DOI : 10.1109/5.97299

URL : https://hal.archives-ouvertes.fr/inria-00075075

P. Fritzson, Principles of Object-Oriented Modeling and Simulation with Modelica 2.1, 2003.
DOI : 10.1109/9780470545669

J. Chr, K. G. Godskesen, A. Larsen, and . Skou, Automatic verification of real-time systems using Epsilon, PSTV, volume 1 of IFIP Conference Proceedings, pp.323-330, 1994.

G. Gössler and J. Raclet, Modal Contracts for Component-Based Design, 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, 2009.
DOI : 10.1109/SEFM.2009.26

S. Graf, R. Passerone, and S. Quinton, Contract-Based Reasoning for Component Systems with Rich Interactions, Embedded Systems Development: From Functional Models to Implementations, pp.139-154, 2014.
DOI : 10.1007/978-1-4614-3879-3_8

S. Graf and S. Quinton, Contracts for BIP: Hierarchical Interaction Models for Compositional Verification, Lecture Notes in Computer Science, vol.4574, pp.1-18
DOI : 10.1007/978-3-540-73196-2_1

O. Grumberg and D. E. Long, Model checking and modular verification, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.843-871, 1994.
DOI : 10.1145/177492.177725

S. Imene-ben-hafaiedh, S. Graf, and . Quinton, Reasoning about Safety and Progress Using Contracts, Proc. of ICFEM'10, pp.436-451, 2010.

N. Halbwachs, Synchronous programming of reactive systems, Kluwer Academic Pub, 1993.

N. Halbwachs, F. Lagnier, and C. Ratel, Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE, IEEE Transactions on Software Engineering, vol.18, issue.9, pp.785-793, 1992.
DOI : 10.1109/32.159839

N. Halbwachs, F. Lagnier, and P. Raymond, Synchronous Observers and the Verification of Reactive Systems, AMAST, Workshops in Computing, pp.83-96, 1993.
DOI : 10.1007/978-1-4471-3227-1_8

N. Halbwachs and P. Raymond, Validation of Synchronous Reactive Systems: From Formal Verification to Automatic Testing, Lecture Notes in Computer Science, vol.1742, pp.1-12, 1999.
DOI : 10.1007/3-540-46674-6_1

D. Harel, Statecharts: a visual formalism for complex systems, Science of Computer Programming, vol.8, issue.3, pp.231-274, 1987.
DOI : 10.1016/0167-6423(87)90035-9

D. Harel, R. Lampert, A. Marron, and G. Weiss, Model-checking behavioral programs, Proceedings of the ninth ACM international conference on Embedded software, EMSOFT '11, pp.279-288, 2011.
DOI : 10.1145/2038642.2038686

D. Harel and R. Marelly, Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine, 2003.
DOI : 10.1007/978-3-642-19029-2

D. Harel, A. Marron, and G. Weiss, Behavioral programming, Communications of the ACM, vol.55, issue.7, pp.90-100, 2012.
DOI : 10.1145/2209249.2209270

D. Harel, A. Marron, G. Wiener, and G. Weiss, Behavioral programming, decentralized control, and multiple time scales, Proceedings of the compilation of the co-located workshops on DSM'11, TMC'11, AGERE!'11, AOOPES'11, NEAT'11, & VMIL'11, SPLASH '11 Workshops, pp.171-182, 2011.
DOI : 10.1145/2095050.2095079

D. Harel and A. Pnueli, On the development of reactive systems Logic and Models for Verification and Specification of Concurrent Systems, volume F13 of NATO ASI Series, pp.477-498, 1985.

A. Thomas, D. Henzinger, and . Nickovic, Independent implementability of viewpoints, Lecture Notes in Computer Science, vol.7539, pp.380-395, 2012.

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

C. B. Jones, Specification and design of (parallel) programs, IFIP Congress, pp.321-332, 1983.

B. Jonsson and K. G. Larsen, Specification and refinement of probabilistic processes, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.266-277, 1991.
DOI : 10.1109/LICS.1991.151651

L. Juhl, K. G. Larsen, and J. Srba, Modal transition systems with weight intervals, The Journal of Logic and Algebraic Programming, vol.81, issue.4, pp.408-421, 2012.
DOI : 10.1016/j.jlap.2012.03.008

G. Kahn, The Semantics of Simple Language for Parallel Programming, IFIP Congress, pp.471-475, 1974.

S. Karris, Introduction to Simulink with Engineering Applications, 2006.

G. Karsai, J. Sztipanovitz, A. Ledczi, and T. Bapty, Modelintegrated development of embedded software, Proceedings of the IEEE, 2003.

O. Kupferman and M. Y. Vardi, Modular Model Checking, COMPOS, pp.381-401, 1997.
DOI : 10.1007/3-540-49213-5_14

L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, vol.3, issue.2, pp.125-143, 1977.
DOI : 10.1109/TSE.1977.229904

C. Larman and V. R. Basili, Iterative and incremental developments. a brief history, Computer, vol.36, issue.6, pp.47-56, 2003.
DOI : 10.1109/MC.2003.1204375

K. G. Larsen, A. Legay, L. Traonouez, and A. Wasowski, Robust synthesis for real-time systems, Theoretical Computer Science, vol.515, pp.96-122, 2014.
DOI : 10.1016/j.tcs.2013.08.015

URL : https://hal.archives-ouvertes.fr/hal-01087778

G. Kim, L. Larsen, and . Xinxin, Equation solving using modal transition systems, Proceedings of the 5th Annual IEEE Symp. on Logic in Computer Science, LICS'90, pp.108-117, 1990.

K. Larsen, Modal specifications, Lecture Notes in Computer Science, vol.407, pp.232-246, 1989.
DOI : 10.1007/3-540-52148-8_19

U. Kim-guldstrand-larsen, A. Nyman, and . Wasowski, Interface Input/Output Automata, Lecture Notes in Computer Science, vol.4085, pp.82-97
DOI : 10.1007/11813040_7

U. Kim-guldstrand-larsen, A. Nyman, and . Wasowski, Modal I/O Automata for Interface and Product Line Theories, Programming Languages and Systems, 16th European Symposium on Programming, ESOP'07, pp.64-79, 2007.
DOI : 10.1007/978-3-540-71316-6_6

U. Kim-guldstrand-larsen, A. Nyman, and . Wasowski, On Modal Refinement and Consistency, Proc. of the 18th International Conference on Concurrency Theory (CONCUR'07), pp.105-119, 2007.

B. Kim-guldstrand-larsen, C. Steffen, and . Weise, A constraint oriented proof methodology based on modal transition systems, Proc. of the 1st International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS'95), pp.17-40, 1995.
DOI : 10.1007/3-540-60630-0_2

K. Larsen and B. Thomsen, A modal process logic, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.203-210, 1988.
DOI : 10.1109/LICS.1988.5119

H. T. Le and R. Passerone, Refinement-based synthesis of correct contract model decompositions, 2014 Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE), 2014.
DOI : 10.1109/MEMCOD.2014.6961851

H. T. , T. Le, R. Passerone, U. Fahrenberg, and A. Legay, A tag contract framework for heterogeneous systems, Proceedings of the 12 th International Workshop on Foundations of Coordination Languages and Self Adaptive Systems, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01087915

H. T. , T. Le, R. Passerone, U. Fahrenberg, and A. Legay, Tag machines for modeling heterogeneous systems, Proceedings of the 13 th International Conference on Application of Concurrency to System Design, ACSD13, pp.186-195, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01087910

A. Ledeczi, A. Bakay, M. Maroti, P. Volgyesi, G. Nordstrom et al., Composing domain-specific design environments, Computer, vol.34, issue.11, pp.44-51, 2001.
DOI : 10.1109/2.963443

A. Ledeczi, M. Maroti, A. Bakay, G. Karsai, J. Garrett et al., The generic modeling environment, Proceedings of the IEEE International Workshop on Intelligent Signal Processing (WISP2001), 2001.

G. Lüttgen and W. Vogler, Modal interface automata, Logical Methods in Computer Science, vol.9, issue.3, p.2013

G. Lüttgen and W. Vogler, Richer interface automata with optimistic and pessimistic compatibility, Acta Informatica, vol.388, issue.1???3, 2013.
DOI : 10.1007/s00236-014-0211-0

N. A. Lynch, Input/Output Automata: Basic, Timed, Hybrid, Probabilistic, Dynamic,..., Lecture Notes in Computer Science, vol.2761, pp.187-188, 2003.
DOI : 10.1007/978-3-540-45187-7_12

N. A. Lynch and E. W. Stark, A proof of the Kahn principle for input/output automata, Information and Computation, vol.82, issue.1, pp.81-92, 1989.
DOI : 10.1016/0890-5401(89)90066-7

Z. Manna and A. Pnueli, Temporal verification of reactive systems: Safety, 1995.
DOI : 10.1007/978-1-4612-4222-2

H. Marchand, P. Bournai, M. L. Borgne, and P. L. Guernic, Synthesis of Discrete-Event Controllers Based on the Signal Environment. Discrete Event Dynamic Systems, pp.325-346, 2000.
URL : https://hal.archives-ouvertes.fr/hal-00546147

H. Marchand and M. Samaan, Incremental design of a power transformer station controller using a controller synthesis methodology, IEEE Transactions on Software Engineering, vol.26, issue.8, pp.729-741, 2000.
DOI : 10.1109/32.879811

URL : https://hal.archives-ouvertes.fr/hal-00546156

B. Meyer, Applying 'design by contract', Computer, vol.25, issue.10, pp.40-51, 1992.
DOI : 10.1109/2.161279

B. Meyer, Touch of Class: Learning to Program Well Using Object Technology and Design by Contract, 2009.
DOI : 10.1007/978-3-540-92145-5

A. Miné, Weakly Relational Numerical Abstract Domains. Phd, Ecole Normale Supérieure, département d'informatique, 2004.

M. W. Maier, Architecting principles for systems-of-systems, Systems Engineering, vol.1, issue.4, pp.267-284, 1998.
DOI : 10.1002/(SICI)1520-6858(1998)1:4<267::AID-SYS3>3.0.CO;2-D

A. Walid, E. A. Najjar, G. R. Lee, and . Gao, Advances in the dataflow computational model, Parallel Computing, vol.25, pp.13-141907, 1999.

R. Negulescu, Process Spaces and the Formal Verification of Asynchronous Circuits, Canada, 1998.

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous data flow programming language LUSTRE, Proceedings of the IEEE, vol.79, issue.9, pp.1305-1320, 1991.
DOI : 10.1109/5.97300

P. Nuzzo, A. Sangiovanni-vincentelli, X. Sun, and A. Puggelli, Methodology for the Design of Analog Integrated Interfaces Using Contracts, IEEE Sensors Journal, vol.12, issue.12, pp.3329-3345, 2012.
DOI : 10.1109/JSEN.2012.2211098

J. Hudak, P. Feiler, and D. Gluch, The Architecture Analysis and Design Language (AADL): An Introduction. Software Engineering Institute (SEI) Technical Note, 2006.

R. Passerone, Semantic Foundations for Heterogeneous Systems, 2004.

R. Passerone, T. A. Luca-de-alfaro, A. L. Henzinger, and . 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

R. Passerone, J. R. Burch, and A. L. Sangiovanni-vincentelli, Refinement preserving approximations for the design and verification of heterogeneous systems, Formal Methods in System Design, vol.170, issue.4, pp.1-33, 2007.
DOI : 10.1007/s10703-006-0024-z

R. Passerone, I. B. Hafaiedh, S. Graf, A. Benveniste, D. Cancila et al., Metamodels in Europe: Languages, Tools, and Applications, Metamodels in Europe: Languages, tools, and applications, pp.38-53, 2009.
DOI : 10.1109/MDT.2009.64

P. Le, G. , T. Gautier, M. L. Borgne, C. L. et al., Programming real-time applications with Signal, Proceedings of the IEEE, pp.1321-1336, 1991.
URL : https://hal.archives-ouvertes.fr/inria-00075114

I. Pill, B. Jobstmann, R. Bloem, R. Frank, M. Moulin et al., Property simulation, 2005.

A. Pinto, A. Bonivento, A. L. Sangiovanni-vincentelli, R. Passerone, and M. Sgroi, System level design paradigms, ACM Transactions on Design Automation of Electronic Systems, vol.11, issue.3, pp.537-563, 2006.
DOI : 10.1145/1142980.1142982

D. Potop-butucaru, B. Caillaud, and A. Benveniste, Concurrency in Synchronous Systems, Formal Methods in System Design, vol.18, issue.2, pp.111-130, 2006.
DOI : 10.1007/s10703-006-7844-8

URL : https://hal.archives-ouvertes.fr/inria-00124252

D. Potop-butucaru, R. De-simone, and Y. Sorel, Necessary and sufficient conditions for deterministic desynchronization, Proceedings of the 7th ACM & IEEE international conference on Embedded software , EMSOFT '07, pp.124-133, 2007.
DOI : 10.1145/1289927.1289950

URL : https://hal.archives-ouvertes.fr/inria-00137885

T. Quatrani, Visual modeling with Rational Rose, p.and UML, 2000.

R. Sudarsan, S. J. Fenves, R. D. Sriram, and F. Wang, A product information modeling framework for product lifecycle management, Computer-Aided Design, vol.37, issue.13, pp.1399-1411, 2005.
DOI : 10.1016/j.cad.2005.02.010

J. Raclet, Quotient de spécifications pour la réutilisation de composants, 2007.

J. Raclet, Residual for Component Specifications, Proc. of the 4th International Workshop on Formal Aspects of Component Software (FACS'07), 2007.
DOI : 10.1016/j.entcs.2008.06.023

URL : https://hal.archives-ouvertes.fr/inria-00141898

J. Raclet, E. Badouel, A. Benveniste, B. Caillaud, A. Legay et al., Modal interfaces, Proceedings of the seventh ACM international conference on Embedded software, EMSOFT '09, pp.87-96, 2009.
DOI : 10.1145/1629335.1629348

URL : https://hal.archives-ouvertes.fr/inria-00555742

J. Raclet, E. Badouel, A. Benveniste, B. Caillaud, A. Legay et al., A modal interface theory for component-based design, Fundamenta Informaticae, vol.108, issue.12, pp.119-149, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00554283

J. Raclet, E. Badouel, A. Benveniste, B. Caillaud, and R. Passerone, Why Are Modalities Good for Interface Theories?, 2009 Ninth International Conference on Application of Concurrency to System Design, 2009.
DOI : 10.1109/ACSD.2009.22

URL : https://hal.archives-ouvertes.fr/inria-00375098

J. Reineke and S. Tripakis, Basic Problems in Multi-View Modeling, TACAS, 2014.
DOI : 10.1007/978-3-642-54862-8_15

P. Reinkemeier and I. Stierand, Compositional timing analysis of realtime systems based on resource segregation abstraction, Embedded Systems: Design, Analysis and Verification -4th IFIP TC 10 International Embedded Systems Symposium, IESS 2013 Proceedings, volume 403 of IFIP Advances in Information and Communication Technology, pp.181-192, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01466672

P. Reinkemeier and I. Stierand, Real-Time Contracts -A Contract Theory Considering Resource Supplies and Demands. Reports of SFB, 2014.

R. Payne and J. Fitzgerald, Evaluation of Architectural Frameworks Supporting Contract-Based Specification, 2010.

R. W. Floyd, Assigning meaning to programs, Proceedings of Symposium on Applied Mathematics, pp.19-32, 1967.

A. Sangiovanni-vincentelli, S. Shukla, J. Sztipanovits, G. Yang, and D. Mathaikutty, Metamodeling: An Emerging Representation Paradigm for System-Level Design, IEEE Design & Test of Computers, vol.26, issue.3, pp.54-69, 2009.
DOI : 10.1109/MDT.2009.62

A. Sangiovanni-vincentelli, Quo Vadis, SLD? Reasoning About the Trends and Challenges of System Level Design, Proc. of the IEEE, pp.467-506, 2007.
DOI : 10.1109/JPROC.2006.890107

A. Sangiovanni-vincentelli, W. Damm, and R. Passerone, Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems*, European Journal of Control, vol.18, issue.3, pp.217-238, 2012.
DOI : 10.3166/ejc.18.217-238

D. Schmidt, Model-driven engineering, IEEE Computer, pp.25-31, 2006.

G. Sibay, S. Uchitel, and V. Braberman, Existential live sequence charts revisited, Proceedings of the 13th international conference on Software engineering , ICSE '08, 2008.
DOI : 10.1145/1368088.1368095

J. Sifakis, Component-Based Construction of Heterogeneous Real-Time Systems in Bip, Petri Nets, p.1, 2009.
DOI : 10.1007/978-3-642-02424-5_1

E. W. Stark, A proof technique for rely/guarantee properties, Lecture Notes in Computer Science, vol.206, pp.369-391, 1985.
DOI : 10.1007/3-540-16042-6_21

I. Stierand, P. Reinkemeier, and P. Bhaduri, Virtual Integration of Real-Time Systems Based on Resource Segregation Abstraction, Formal Modeling and Analysis of Timed Systems -12th International Conference, FOR- MATS 2014, pp.206-221, 2014.
DOI : 10.1007/978-3-319-10512-3_15

I. Stierand, P. Reinkemeier, T. Gezgin, and P. Bhaduri, Real-time scheduling interfaces and contracts for the design of distributed embedded systems, 2013 8th IEEE International Symposium on Industrial Embedded Systems (SIES), pp.130-139, 2013.
DOI : 10.1109/SIES.2013.6601485

S. Tripakis, B. Lickly, T. A. Henzinger, and E. A. Lee, On relational interfaces, Proceedings of the seventh ACM international conference on Embedded software, EMSOFT '09, pp.67-76, 2009.
DOI : 10.1145/1629335.1629346

S. Tripakis, B. Lickly, T. A. Henzinger, and E. A. Lee, A Theory of Synchronous Relational Interfaces, ACM Transactions on Programming Languages and Systems, vol.33, issue.4, p.14, 2011.
DOI : 10.1145/1985342.1985345

S. Uchitel and M. Chechik, Merging partial behavioural models, Proc. of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT FSE'10), pp.43-52, 2004.

J. Warmer and A. Kleppe, The Object Constraint Language: Getting Your Models Ready for MDA, 2003.

E. S. Wolf, Hierarchical Models of Synchronous Circuits for Formal Verification and Substitution, 1995.