T. Abdellatif, J. Combaz, and J. Sifakis, Model-based implementation of realtime applications, EMSOFT, pp.229-238, 2010.

L. D. Alfaro and T. A. Henzinger, Interface Theories for Component-Based Design, EMSOFT, pp.148-165, 2001.
DOI : 10.1007/3-540-45449-7_11

R. Alur and T. A. Henzinger, Reactive modules. Form, Formal Methods in System Design, vol.15, issue.1, pp.7-48, 1999.
DOI : 10.1023/A:1008739929481

F. Balarin, L. Lavagno, C. Passerone, A. Sangiovanni-vincentelli, M. Sgroi et al., Modeling and Designing Heterogeneous Systems, p.66
DOI : 10.1007/3-540-36190-1_7

T. Ball, B. Cook, V. Levin, and S. K. Rajamani, SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft, In IFM, pp.1-20, 2004.
DOI : 10.1007/978-3-540-24756-2_1

T. Ball and S. K. Rajamani, The SLAM Toolkit, CAV, pp.260-264, 2001.
DOI : 10.1007/3-540-44585-4_25

T. Ball and S. K. Rajamani, The SLAM project: debugging system software via static analysis, POPL, pp.1-3, 2002.

A. Basu, S. Bensalem, M. Bozga, P. Bourgos, M. Maheshwari et al., Component Assemblies in the Context of Manycore, FMCO, pp.314-333, 2011.
DOI : 10.1007/3-540-16042-6_21
URL : https://hal.archives-ouvertes.fr/hal-00878716

A. Basu, S. Bensalem, M. Bozga, B. Caillaud, B. Delahaye et al., Statistical abstraction and model-checking of large heterogeneous systems, In FMOODS/FORTE LNCS, vol.6117, pp.32-46, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01055148

A. Basu, S. Bensalem, M. Bozga, J. Combaz, M. Jaber et al., Rigorous Component-Based System Design Using the BIP Framework, IEEE Software, vol.28, issue.3, pp.41-48, 2011.
DOI : 10.1109/MS.2011.27
URL : https://hal.archives-ouvertes.fr/hal-00722395

A. Basu, S. Bensalem, M. Bozga, B. Delahaye, A. Legay et al., Verification of an AFDX Infrastructure Using Simulations and Probabilities, RV, pp.330-344, 2010.
DOI : 10.1007/978-3-642-16612-9_25

A. Basu, M. Bozga, and J. Sifakis, Modeling Heterogeneous Real-time Components in BIP, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), pp.3-12, 2006.
DOI : 10.1109/SEFM.2006.27
URL : https://hal.archives-ouvertes.fr/hal-00375298

A. Basu, L. Mounier, M. Poulhis, J. Pulou, and J. Sifakis, Using BIP for modeling and verification of networked systems -a case study on tinyos-based Title Suppressed Due to Excessive Length 67 networks, NCA, pp.257-260, 2007.

S. Bensalem, M. Bozga, B. Delahaye, C. Jegourel, A. Legay et al., Statistical Model Checking QoS Properties of Systems with SBIP, ISOLA, pp.327-341, 2012.
DOI : 10.1007/978-3-642-34026-0_25
URL : https://hal.archives-ouvertes.fr/hal-01087822

S. Bensalem, M. Bozga, A. Legay, T. Nguyen, J. Sifakis et al., Incremental component-based construction and verification using invariants, FMCAD, pp.257-265, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00557802

S. Bensalem, M. Bozga, T. Nguyen, and J. Sifakis, Compositional verification for component-based systems and application, ATVA, pp.64-79
URL : https://hal.archives-ouvertes.fr/hal-00568866

S. Bensalem, M. Bozga, T. Nguyen, and J. Sifakis, D-Finder: A Tool for Compositional Deadlock Detection and Verification, CAV, pp.614-619
DOI : 10.1007/978-3-642-02658-4_45
URL : https://hal.archives-ouvertes.fr/hal-00722550

S. Bensalem, M. Bozga, T. Nguyen, and J. Sifakis, Compositional verification for component-based systems and application, IET Software, vol.4, pp.179-235, 2010.
DOI : 10.1049/iet-sen.2009.0011
URL : https://hal.archives-ouvertes.fr/hal-00568866

S. Bensalem, L. De-silva, M. Gallien, F. Ingrand, and R. Yan, Rock solid " software: A verifiable and correct by construction controller for rover and spacecraft functional layers, ISAIRAS, pp.859-866, 2010.

S. Bensalem, L. De-silva, A. Griesmayer, F. Ingrand, A. Legay et al., A Formal Approach for Incremental Construction with an Application to Autonomous Robotic Systems, In SC, vol.14, issue.4, pp.116-132, 2011.
DOI : 10.1002/rob.20206

S. Bensalem, M. Gallien, F. Ingrand, I. Kahloul, and T. Nguyen, Toward a more dependable software architecture for autonomous robots, IEEE Robotics and Automation Magazine, vol.16, issue.1, pp.1-11, 2009.

S. Bensalem, A. Griesmayer, A. Legay, T. Nguyen, and D. Peled, Efficient deadlock detection for concurrent systems, Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011), pp.119-129, 2011.
DOI : 10.1109/MEMCOD.2011.5970518

S. Bensalem, A. Legay, T. Nguyen, J. Sifakis, and R. Yan, Incremental Invariant Generation for Compositional Design, 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, pp.157-167, 2010.
DOI : 10.1109/TASE.2010.23

D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, The software model checker Blast, International Journal on Software Tools for Technology Transfer, vol.2, issue.4, pp.5-6505, 2007.
DOI : 10.1007/s10009-007-0044-z

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

M. Bozga, M. Jaber, N. Maris, and J. Sifakis, Modeling Dynamic Architectures Using Dy-BIP, In SC, pp.1-16, 2012.
DOI : 10.1007/978-3-642-30564-1_1
URL : https://hal.archives-ouvertes.fr/hal-00722481

M. Bozga, V. Sfyrla, and J. Sifakis, Modeling synchronous systems in BIP, Proceedings of the seventh ACM international conference on Embedded software, EMSOFT '09, pp.77-86, 2009.
DOI : 10.1145/1629335.1629347
URL : https://hal.archives-ouvertes.fr/hal-00722479

K. M. Chandy, Parallel Program Design, 1988.
DOI : 10.1007/978-1-4613-9668-0_6

M. R. Chaudron, E. M. Eskenazi, A. V. Fioukov, and D. K. Hammer, A framework for formal component-based software architecting, SAVCBS, Title Suppressed Due to Excessive Length, pp.73-80, 2001.

A. Cheng, J. Esparza, and J. Palsberg, Complexity results for 1-safe nets, FSTTCS, pp.326-337, 1993.

A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, NUSMV: a new symbolic model checker, International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.4, pp.410-425, 2000.
DOI : 10.1007/s100090050046

E. M. Clarke, O. Grumberg, and D. A. , Peled. Model checking, 1999.

J. M. Cobleigh, G. S. Avrunin, and L. A. Clarke, Breaking up is hard to do, ACM Transactions on Software Engineering and Methodology, vol.17, issue.2, pp.1-52, 2008.
DOI : 10.1145/1348250.1348253

J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu, Learning Assumptions for Compositional Verification, TACAS, pp.331-346, 2003.
DOI : 10.1007/3-540-36577-X_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.913

C. L. Conway, K. S. Namjoshi, D. Dams, and S. A. Edwards, Incremental Algorithms for Inter-procedural Analysis of Safety Properties, CAV, pp.449-461, 2005.
DOI : 10.1007/11513988_45

B. Cook, A. Podelski, and A. Rybalchenko, Terminator: Beyond Safety, CAV, pp.415-418, 2006.
DOI : 10.1007/11817963_37
URL : http://hdl.handle.net/11858/00-001M-0000-000F-2418-5

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

W. De-roever, F. De-boer, U. Hannemann, J. Hooman, Y. Lakhnech et al., Concurrency Verification: Introduction to Compositional and Noncompositional Methods, 2000.

B. Dutertre and L. De-moura, A Fast Linear-Arithmetic Solver for DPLL(T), CAV, pp.81-94, 2006.
DOI : 10.1007/11817963_11

A. Farzan, Y. Chen, E. M. Clarke, Y. Tsay, and B. Wang, Extending??Automated??Compositional??Verification to the Full Class of Omega-Regular Languages, TACAS, pp.2-17, 2008.
DOI : 10.1007/978-3-540-78800-3_2

C. Flanagan and S. Qadeer, Thread-Modular Model Checking, SPIN, pp.213-224, 2003.
DOI : 10.1007/3-540-44829-2_14

S. Fleury, M. Herrb, and R. Chatila, GenoM: A Tool for the Specification and the Implementation of Operating Modules in a Distributed Robot Architecture, IROS, pp.842-848, 1997.

P. Fritzson and V. Engelson, Modelica ??? A unified object-oriented language for system modeling and simulation, ECOOP, pp.67-90, 1998.
DOI : 10.1007/BFb0054087

D. Giannakopoulou, C. S. , and H. Barringer, Assumption generation for software component verification, Proceedings 17th IEEE International Conference on Automated Software Engineering,, pp.3-12, 2002.
DOI : 10.1109/ASE.2002.1114984

G. Gößler and J. Sifakis, Priority Systems, In FMCO, vol.3, issue.1, pp.314-329, 2003.
DOI : 10.1145/353323.353382

A. Gupta, C. Popeea, and A. Rybalchenko, Predicate abstraction and refinement for verifying multi-threaded programs, POPL, pp.331-344, 2011.

D. Heimbold and D. Luckham, Debugging Ada Tasking Programs, IEEE Software, vol.2, issue.2, pp.47-57, 1985.
DOI : 10.1109/MS.1985.230351

T. A. Henzinger, T. Hottelier, L. Kovács, and A. Rybalchenko, Aligators for arrays, LPAR, TACAS 2010, pp.348-356, 2010.

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, Lazy abstraction, POPL, pp.58-70, 2002.
DOI : 10.1145/565816.503279

T. A. Henzinger, S. Qadeer, and S. K. Rajamani, You assume, we guarantee: Methodology and case studies, CAV, pp.440-451, 1998.
DOI : 10.1007/BFb0028765
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.110.7757

M. Hermenegildo, G. Puebla, K. Marriott, and P. J. Stuckey, Incremental analysis of constraint logic programs, ACM Transactions on Programming Languages and Systems, vol.22, issue.2, pp.187-223, 2000.
DOI : 10.1145/349214.349216

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

F. Khendek and G. V. Bochmann, Incremental construction approach for distributed system specifications, Proceedings of the Int. Symp. on Formal Description Techniques, pp.26-29, 1993.

K. G. Larsen, Modal specifications, Automatic Verification Methods for Finite State Systems, pp.232-246, 1989.
DOI : 10.1007/3-540-52148-8_19

K. Lau, K. Ng, T. Rana, and C. M. Tran, Incremental construction of component-based systems, Proceedings of the 15th ACM SIGSOFT symposium on Component Based Software Engineering, CBSE '12, pp.41-50
DOI : 10.1145/2304736.2304746

N. A. Lynch and M. R. Tuttle, An introduction to input/output automata, CWI Quarterly, vol.2, pp.219-246, 1989.

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

L. D. Moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

T. Nguyen, Constructive Verification of Component-based Systems, 2010.

A. Pnueli, In transition from global to modular temporal reasoning about programs. Logics and models of concurrent systems, pp.123-144, 1985.

C. Popeea and A. Rybalchenko, Compositional termination proofs for multithreaded programs, TACAS, pp.237-251, 2012.

J. Queille and J. Sifakis, Specification and verification of concurrent systems in CESAR, ICALP, pp.337-351, 1982.
DOI : 10.1007/3-540-11494-7_22

F. Somenzi, CUDD: CU decision diagram package

O. Team, The Omega library, 1996.

L. Thiele, I. Bacivarov, W. Haid, and K. Huang, Mapping Applications to Tiled Multiprocessor Embedded Systems, Seventh International Conference on Application of Concurrency to System Design (ACSD 2007), pp.29-40, 2007.
DOI : 10.1109/ACSD.2007.53

S. Tripakis, C. Stergiou, C. Shaver, and E. A. Lee, A modular formal semantics for Ptolemy, Mathematical Structures in Computer Science, vol.218, issue.04, 2012.
DOI : 10.1016/0304-3975(94)00202-T