A. Benveniste and G. Berry, The synchronous approach to reactive and real-time systems. Readings in hardware/software co-design, pp.147-159, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00075115

M. Caporuscio, P. Inverardi, and P. Pelliccione, Compositional verification of middleware-based software architecture descriptions, Proceedings. 26th International Conference on Software Engineering, 2004.
DOI : 10.1109/ICSE.2004.1317444

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore et al., NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Proceeeding CAV, number 2404 in LNCS, pp.359-364, 2002.
DOI : 10.1007/3-540-45657-0_29

E. M. Clarke, E. A. Emerson, and A. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, pp.244-263, 1986.
DOI : 10.1145/5397.5399

G. Delaval-andéricand´andéric-rutten, Reactive model-based control of reconfiguration in the fractal component-based model Available from, 13th International Symposium on Component Based Software Engineering, 2010.

P. Grace, Dynamic Adaptation, Middleware for Network Eccentric and Mobile Applications, pp.285-304, 2009.
DOI : 10.1007/978-3-540-89707-1_13

N. Halbwachs, F. Lagnier, and P. Raymond, Synchronous Observers and the Verification of Reactive Systems, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93 Workshops in Computing, 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, ASIAN'99, Asian Computing Science Conference, 1999.
DOI : 10.1007/3-540-46674-6_1

G. J. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1997.
DOI : 10.1109/32.588521

V. Issarny, M. Caporuscio, and N. Georgantas, A Perspective on the Future of Middleware-based Software Engineering, Future of Software Engineering (FOSE '07)
DOI : 10.1109/FOSE.2007.2

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

J. Hugues, L. Pautet, and F. Kordon, Refining middleware functions for verification purpose, Proceedings of the Monterey Workshop 2003 (MON- TEREY'03), pp.79-87, 2003.

E. M. Clarke-jr, O. Grumberg, and D. E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems, vol.16, issue.5, pp.1512-1542, 1994.
DOI : 10.1145/186025.186051

P. K. Mckinley, S. Masoud-sadjadi, E. P. Kasten, and B. H. Cheng, Composing adaptive software Available from: http://portal.acm.org/citation.cfm?id= 1008751, IEEE Computer, vol.371008762, issue.7, pp.56-6448, 2004.

G. Mealy, A method for synthesizing sequential circuits, The Bell System Technical Journal, vol.34, issue.5, pp.1045-1079, 1955.
DOI : 10.1002/j.1538-7305.1955.tb03788.x

F. Lagnier, N. Halbwachs, and C. , Programming and verifying critical systems by means of the synchronous data-flow programming language lustre . Special Issue on the Specification and Analysis of Real-Time Systems, IEEE Transactions on Software Engineering, 1992.

S. Nakajima, Verification of Web service flows with model-checking techniques, First International Symposium on Cyber Worlds, 2002. Proceedings., p.378, 2002.
DOI : 10.1109/CW.2002.1180904

J. Tigli, S. Lavirotte, G. Rey, V. Hourdin, and M. , Lightweight service oriented architecture for pervasive computing, IJCSI International Journal of Computer Science Issues, vol.4, issue.1, pp.1694-0784, 2009.

N. Venkatasubramanian, C. Talcott, and G. A. Agha, A formal model for reasoning about adaptive QoS-enabled middleware, ACM Transactions on Software Engineering and Methodology, vol.13, issue.1, pp.86-147, 2004.
DOI : 10.1145/1005561.1005564

M. Weiser, The Computer for the 21st Century, Scientific American, vol.265, issue.3, pp.94-104, 1991.
DOI : 10.1038/scientificamerican0991-94