R. Allen, A Formal Approach to Software Architecture, Carnegie Mellon, School of Computer Science, 1997.

R. Allen and D. Garlan, A formal basis for architectural connection, ACM Transactions on Software Engineering and Methodology, vol.6, issue.3, pp.213-249, 1997.
DOI : 10.1145/258077.258078

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

F. Arbab, The IWIM model for coordination of concurrent activities, Lecture Notes in Computer Science, vol.1061, pp.34-56, 1996.
DOI : 10.1007/3-540-61052-9_38

F. Arbab, Reo: a channel-based coordination model for component composition, Mathematical Structures in Computer Science, vol.14, issue.3, pp.329-366, 2004.
DOI : 10.1017/S0960129504004153

F. Arbab, Abstract Behavior Types: a foundation model for components and their composition, Science of Computer Programming, vol.55, issue.1-3, pp.3-52, 2005.
DOI : 10.1016/j.scico.2004.05.010

F. Arbab, M. M. Bonsangue, and F. S. De-boer, A coordination lanuage for mobile components, pp.166-173, 2000.

F. Arbab, T. Chothia, R. Mei, S. Meng, Y. Moon et al., From Coordination to Stochastic Models of QoS, COORDINATION '09: Proceedings of the 11th International Conference on Coordination Models and Languages, pp.268-287, 2009.
DOI : 10.1007/978-1-4615-2367-3

F. Arbab, T. Chothia, S. Meng, and Y. Moon, Component Connectors with QoS Guarantees, Lecture Notes in Computer Science, vol.4467, pp.286-304, 2007.
DOI : 10.1007/978-3-540-72794-1_16

F. Arbab, F. S. De-boer, and M. M. Bonsangue, A Logical Interface Description Language for Components, Lecture Notes in Computer Science, vol.21, issue.4, pp.249-266, 1906.
DOI : 10.1109/32.385970

F. Arbab, S. Meng, Y. Moon, M. Kwiatkowska, and H. Qu, Reo2MC, Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering on European software engineering conference and foundations of software engineering symposium, ESEC/FSE '09, pp.287-288, 2009.
DOI : 10.1145/1595696.1595745

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

A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, Verifying continuous time Markov chains, Proc. 8th International Conference on Computer Aided Verification (CAV'96), volume 1102 of LNCS, pp.269-276, 1996.
DOI : 10.1007/3-540-61474-5_75

A. Aziz, V. Singhal, F. Balarin, R. Brayton, and A. Sangiovanni-vincentelli, It usually works: The temporal logic of stochastic systems, Proc. 7th International Conference on Computer Aided Verification (CAV'95), pp.155-165, 1995.
DOI : 10.1007/3-540-60045-0_48

C. Baier, Probabilistic models for reo connector circuits, Journal of Universal Computer Science, vol.11, issue.10, pp.1718-1748, 2005.

C. Baier, J. Katoen, and H. Hermanns, Approximate symbolic model checking of continuoustime Markov chains, Proc. 10th International Conference on Concurrency Theory (CONCUR'99), volume 1664 of LNCS, pp.146-161, 1999.

C. Baier, M. Sirjani, F. Arbab, and J. J. Rutten, Modeling component connectors in Reo by constraint automata, Science of Computer Programming, vol.61, issue.2, pp.75-113, 2006.
DOI : 10.1016/j.scico.2005.10.008

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

G. Berry and G. Boudol, The chemical abstract machine, POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.81-94, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00075426

A. Bianco and L. De-alfaro, Model checking of probabilistic and nondeterministic systems, Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science, pp.499-513, 1995.
DOI : 10.1007/3-540-60692-0_70

P. Bidinger, A. Schmitt, and J. Stefani, An Abstract Machine for the Kell Calculus, Lecture Notes in Computer Science, vol.3535, pp.31-46
DOI : 10.1007/3-540-47959-7_3

P. Bidinger and J. Stefani, The Kell Calculus: Operational Semantics and Type System, FMOODS, pp.109-123, 2003.
DOI : 10.1007/3-540-47959-7_3

S. Bistarelli, U. Montanari, and F. Rossi, Semiring-based constraint satisfaction and optimization, Journal of the ACM, vol.44, issue.2, pp.201-236, 1997.
DOI : 10.1145/256303.256306

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. Calinescu, Implementation of a Generic Autonomic Framework, Fourth International Conference on Autonomic and Autonomous Systems (ICAS'08), pp.124-129, 2008.
DOI : 10.1109/ICAS.2008.21

R. Calinescu and M. Kwiatkowska, Using quantitative analysis to implement autonomic IT systems, 2009 IEEE 31st International Conference on Software Engineering, pp.100-110, 2009.
DOI : 10.1109/ICSE.2009.5070512

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

L. Cardelli and A. D. Gordon, Mobile ambients, FoSSaCS Lecture Notes in Computer Science, vol.1378, pp.140-155, 1998.
DOI : 10.1007/BFb0053547

T. Chothia and J. Kleijn, Q-Automata: Modelling the Resource Usage of Concurrent Components, Electronic Notes in Theoretical Computer Science, vol.175, issue.2, pp.153-167, 2007.
DOI : 10.1016/j.entcs.2007.03.009

A. Condon, The complexity of stochastic games. Information and Computation, pp.203-224, 1992.

C. Courcoubetis and M. Yannakakis, Verifying temporal properties of finite-state probabilistic programs, [Proceedings 1988] 29th Annual Symposium on Foundations of Computer Science, pp.338-345, 1988.
DOI : 10.1109/SFCS.1988.21950

C. Courcoubetis and M. Yannakakis, Markov decision processes and regular events, Proc. 17th International Colloquium on Automata, Languages and Programming (ICALP'90), pp.336-349, 1990.

C. Courcoubetis and M. Yannakakis, The complexity of probabilistic verification, Journal of the ACM, vol.42, issue.4, pp.857-907, 1995.
DOI : 10.1145/210332.210339

L. De-alfaro, Formal Verification of Probabilistic Systems, 1997.

L. De-alfaro, Computing Minimum and Maximum Reachability Times in Probabilistic Systems, Proc. 10th International Conference on Concurrency Theory (CON- CUR'99), pp.66-81, 1999.
DOI : 10.1007/3-540-48320-9_7

L. De-alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala, Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation, Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of LNCS, pp.395-410, 2000.

K. Etessami, M. Kwiatkowska, M. Vardi, and M. Yannakakis, Multi-objective model checking of Markov decision processes, Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), pp.50-65, 2007.

E. M. Hahn, H. Hermanns, and L. Zhang, Probabilistic Reachability for Parametric Markov Models, SPIN, pp.88-106, 2009.
DOI : 10.1007/11691372_26

H. Hansson and B. Jonsson, A logic for reasoning about time and reliability, Formal Aspects of Computing, vol.2, issue.1, pp.512-535, 1994.
DOI : 10.1007/BF01211866

T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic model checking for real-time systems, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.394-406, 1992.
DOI : 10.1109/LICS.1992.185551

A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker, PRISM: A Tool for Automatic Verification of Probabilistic Systems, Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), pp.441-444, 2006.
DOI : 10.1007/11691372_29

P. Inverardi, P. Pelliccione, and M. Tivoli, Towards an assume-guarantee theory for adaptable systems, 2009 ICSE Workshop on Software Engineering for Adaptive and Self-Managing Systems, 2009.
DOI : 10.1109/SEAMS.2009.5069079

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

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, A game-based abstraction-refinement framework for??Markov decision processes, Formal Methods in System Design, vol.58, issue.1???2, 2008.
DOI : 10.1007/s10703-010-0097-6

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, Abstraction Refinement for Probabilistic Software, Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), 2009.
DOI : 10.1007/978-3-540-93900-9_17

M. Kwiatkowska, G. Norman, and D. Parker, Game-based abstraction for Markov decision processes, Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST'06), pp.157-166, 2006.

M. Kwiatkowska, G. Norman, and D. Parker, Stochastic Games for Verification of Probabilistic Timed Automata, Proc. 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'09), pp.212-227
DOI : 10.1007/s10703-005-1632-8

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

M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, Automatic verification of real-time systems with discrete probability distributions, Theoretical Computer Science, vol.282, issue.1, pp.101-150, 2002.
DOI : 10.1016/S0304-3975(01)00046-9

N. R. Mehta, N. Medvidovic, and S. Phadke, Towards a taxonomy of software connectors, Proceedings of the 22nd international conference on Software engineering , ICSE '00, pp.178-187, 2000.
DOI : 10.1145/337180.337201

R. Milner, A Calculus of Communicating Systems, 1982.
DOI : 10.1007/3-540-10235-3

R. Milner, Communicating and Mobile Systems: the Pi-Calculus, 1999.

R. Milner, The Space and Motion of Communicating Agents, 2009.
DOI : 10.1017/CBO9780511626661

R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, I, Information and Computation, vol.100, issue.1, pp.1-40, 1992.
DOI : 10.1016/0890-5401(92)90008-4

R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, II, Information and Computation, vol.100, issue.1, pp.41-77, 1992.
DOI : 10.1016/0890-5401(92)90009-5

R. D. Nicola, G. L. Ferrari, U. Montanari, R. Pugliese, and E. Tuosto, A Process Calculus for QoS-Aware Applications, Lecture Notes in Computer Science, vol.38, issue.6, pp.33-48, 2005.
DOI : 10.1145/1023646.1023648

C. Pasareanu, D. Giannakopoulou, M. Bobaru, J. Cobleigh, and H. Barringer, Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design, pp.175-205, 2008.

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

A. W. Roscoe, The Theory and Practice of Concurrency, 1998.

A. Schmitt and J. Stefani, The Kell Calculus: A Family of Higher-Order Distributed Process Calculi, Global Computing, pp.146-178, 2004.
DOI : 10.1007/3-540-45694-5_19

R. Segala, Modelling and Verification of Randomized Distributed Real Time Systems, 1995.

R. Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, 2005.

R. Segala and N. Lynch, Probabilistic simulations for probabilistic processes, Nordic Journal of Computing, vol.2, issue.2, pp.250-273, 1995.

L. S. Shapley, Stochastic Games, Proceedings of the National Academy of Sciences, vol.39, issue.10, pp.1095-1100, 1953.
DOI : 10.1073/pnas.39.10.1953

M. Shaw and D. Garlan, Software architecture: perspectives on an emerging discipline, 1996.

J. Sifakis, A framework for component-based construction extended abstract, SEFM '05: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, pp.293-300, 2005.

J. Stefani, A calculus of Kells, Electronic Notes in Theoretical Computer Science, vol.85, issue.1, 2003.
DOI : 10.1016/S1571-0661(05)80087-8

S. Tripakis, Te formal analysis of timed systems in practice, 1998.

D. Wallace, Groups, Rings & Fields, CONNECT, vol.231167, p.104104, 1998.
DOI : 10.1007/978-1-4471-0425-4