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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.33.4928

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.

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), 2012.
DOI : 10.1109/CDC.2012.6426437

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

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.5461

. Vardi, Alternating refinement relations, Proc. of the 9th International Conference on Concurrency Theory (CONCUR'98), pp.163-178, 1998.

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, J. R. Burch, L. Lavagno, Y. Watanabe, R. Passerone et al., Constraints specification at higher levels of abstraction, Sixth IEEE International High-Level Design Validation and Test Workshop, pp.129-133, 2001.
DOI : 10.1109/HLDVT.2001.972819

F. Balarin, A. Davare, D. Massimiliano, D. Angelo, T. Densmore et al., Platform-Based Design and Frameworks, Model-Based Design for Embedded Systems, p.259, 2009.
DOI : 10.1201/9781420067859-c10

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.330.3309

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

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

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, 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ý, 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ý, 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, 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, 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

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.133.9343

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

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, 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, 1993.
DOI : 10.1109/TII.2010.2043741

P. Cerný, 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, Lecture Notes in Computer Science, vol.2404, pp.428-441, 2002.
DOI : 10.1007/3-540-45657-0_35

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.7.403

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.126.266

A. Chakrabarti, T. A. Luca-de-alfaro, M. Henzinger, and . Stoelinga, Resource Interfaces, Lecture Notes in Computer Science, vol.2855, pp.117-133, 2003.
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, 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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.111.7245

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.5472

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.

W. Damm and B. Westphal, Live and let die: LSC based verification of UML models, Science of Computer Programming, vol.55, issue.1-3, pp.117-159, 2005.
DOI : 10.1016/j.scico.2004.05.013

A. Davare, D. Densmore, T. Meyerowitz, A. Pinto, A. Sangiovanni-vincentelli et al., A next-generation design framework for platform-based design, Design Verification Conference (DVCon), 2007.

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

URL : http://vbn.aau.dk/ws/files/58768871/HSCC2010cameraready.pdf

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, 2003.

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 component-based design, Lecture Notes in Computer Science, vol.2211, pp.148-165, 2001.

T. A. Luca-de-alfaro, M. Henzinger, and . Stoelinga, Timed Interfaces, Proc. of the 2nd International Workshop on Embedded Software (EMSOFT'02), volume 2491 of Lecture Notes in Computer Science, pp.108-122, 2002.
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ît-delahaye, A. Caillaud, and . Legay, Probabilistic Contracts : A Compositional Reasoning Methodology for the Design of Stochastic Systems, Proc. 10th International Conference on Application of Concurrency to System Design (ACSD), 2010.

B. Benoî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î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î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

D. Densmore, S. Rekhi, and A. L. Sangiovanni-vincentelli, Microarchitecture development via metropolis successive platform refinement, Proceedings Design, Automation and Test in Europe Conference and Exhibition, pp.346-351, 2004.
DOI : 10.1109/DATE.2004.1268871

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.2600

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.534.5100

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

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

D. Fischbein and S. Uchitel, On correct and complete strong merging of partial behaviour models Weaving executability into object-oriented meta-languages, Proc. of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT FSE'08) Proceedgins of the 8 th International Conference on Model Driven Engineering Languages and Systems (MODELS05), pp.297-307, 2005.

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

T. Gezgin, R. Weber, and M. Girod, A Refinement Checking Technique for Contract-Based Architecture Designs, Fourth International Workshop on Model Based Architecting and Construction of Embedded Systems, ACES-MB'11, 2011.

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 and S. Quinton, Contracts for BIP: Hierarchical Interaction Models for Compositional Verification, Lecture Notes in Computer Science, vol.4574, pp.1-18, 2007.
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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.6959

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, H. Kugler, S. Maoz, and I. Segall, Accelerating Smart Play-Out, SOFSEM, pp.477-488, 2010.
DOI : 10.1007/978-3-642-11266-9_40

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.157.2103

D. Harel, R. Lampert, A. Marron, and G. Weiss, Modelchecking behavioral programs, EMSOFT, pp.279-288, 2011.

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.261.373

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.220.9178

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.

H. Heinecke, W. Damm, B. Josko, A. Metzner, H. Kopetz et al., Software Components for Reliable Automotive Systems, Design, Automation and Test in Europe, pp.8-549, 2008.
DOI : 10.1109/date.2008.4484733

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

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. Sztipanovits, A. Ledeczi, and T. Bapty, Model-integrated development of embedded software, Proceedings of the IEEE, vol.91, issue.1, pp.145-164, 2003.
DOI : 10.1109/JPROC.2002.805824

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

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, 2006.
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

B. Kim-guldstrand-larsen, C. Steffen, and . Weise, A constraint oriented proof methodology based on modal transition systems

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

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

URL : http://real.mtak.hu/4598/1/1116623.pdf

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.

E. A. Lee, Cyber Physical Systems: Design Challenges, 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC), 2008.
DOI : 10.1109/ISORC.2008.25

URL : http://chess.eecs.berkeley.edu/pubs/427/Lee_CyberPhysical_ISORC.pdf

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.72.7831

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

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.5059

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

M. Object and . Group, A UML profile for MARTE, beta 1. OMG Adopted Specification ptc, 2007.

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, 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, T. A. Luca-de-alfaro, A. Henzinger, and . Sangiovanni-vincentelli, Convertibility verification and converter synthesis, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design , ICCAD '02, 2002.
DOI : 10.1145/774572.774592

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-00540460

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

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, 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

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.
DOI : 10.1007/978-94-011-1793-7_4

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

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.225.4313

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

URL : http://bsd7.cs.sunysb.edu:18080/~stark/REPORTS/relyguar-revised.ps.gz

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.1522

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.
DOI : 10.1145/1041685.1029904

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.4666

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