Abstract
Nowadays, adaptive middleware plays an important role in the design of applications in ubiquitous and ambient computing. Currently most of these systems manage the adaptation at the middleware intermediary layer. Dynamic adaptive middleware are then decomposed into two levels : a first one to simplify the development of distributed systems using devices, a second one to perform dynamic adaptations within the first level. In this paper we consider component-based middleware and a corresponding compositional adaptation. Indeed, the composition often involves conflicts between concurrent adaptations. Thus we study how to maintain consistency of the application in spite of changes of critical components and conflicts that may appear when we compose some component assemblies. Relying on formal methods, we provide a well defined representation of component behaviors. In such a setting, model checking techniques are applied to ensure that concurrent access does not violate expected and acceptable behaviors of critical components.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
In: ARM 2010: Proceedings of the 9th International Workshop on Adaptive and Reflective Middleware. ACM, New York (2010)
Caporuscio, M., Inverardi, P., Pelliccione, P.: Compositional verification of middleware-based software architecture descriptions. In: ICSE 2004: Proceedings of the 26th International Conference on Software Engineering, pp. 221–230. IEEE, Washington, DC, USA (2004)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002), http://nusmv.irst.itc.it
Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A., Raskin, J.-F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, ICSE 2010, vol. 1, pp. 335–344. ACM, New York (2010), http://doi.acm.org/10.1145/1806799.1806850 http://doi.acm.org/10.1145/1806799.1806850
Delaval, G., Rutten, É.: Reactive model-based control of reconfiguration in the fractal component-based model. In: 13th International Symposium on Component Based Software Engineering (CBSE 2010), Prague, Czech Republic (June 2010), http://pop-art.inrialpes.fr/people/delaval/pub/delaval-cbse10.pdf
Fisler, K., Krishnamurthi, S.: Modular verification of collaboration-based software designs. In: Proceedings of the 8th European Software Engineering Conference held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Vienna, Austria. ESEC/FSE-9, pp. 152–163. ACM, New York (2001), http://doi.acm.org/10.1145/503209.503231 , doi:10.1145/503209.503231
Grace, P.: Dynamic adaptation. In: Miranda, H., Garbinato, B., Rodrigues, L. (eds.) Middleware for Network Eccentric and Mobile Applications, pp. 285–304. Springer, Heidelberg (2009)
Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST 1993. Springer, Heidelberg (1993)
Halbwachs, N., Raymond, P.: Validation of synchronous reactive systems: From formal verification to automatic testing. In: Thiagarajan, P.S., Yap, R.H.C. (eds.) ASIAN 1999. LNCS, vol. 1742, p. 1. Springer, Heidelberg (1999)
Issarny, V., Caporuscio, M., Georgantas, N.: A perspective on the future of middleware-based software engineering. In: 2007 Future of Software Engineering, pp. 244–258. IEEE Computer Society Press, Los Alamitos (2007), http://dx.doi.org/10.1109/FOSE.2007.2 http://dx.doi.org/10.1109/FOSE.2007.2
Hugues, J., Pautet, L., Kordon, F.: Refining middleware functions for verification purpose. In: Proceedings of the Monterey Workshop 2003 (MONTEREY 2003), Chicago, IL, USA, pp. 79–87 (September 2003)
Clarke Jr., E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions om Programming Languages and Systems 16(5), 1512–1542 (1994)
Clarke Jr., E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
McKinley, P.K., Sadjadi, S.M., Kasten, E.P., Cheng, B.H.C.: Composing adaptive software. IEEE Computer 37(7), 56–64 (2004), http://portal.acm.org/citation.cfm?id=1008751.1008762 , doi:10.1109/MC.2004.48
Mealy, G.: A method to synthesizing sequential circuits. Bell Systems Technical Journal, 1045–1079 (1955)
Lagnier, F., Halbwachs, C.R.N.: Programming and verifying critical systems by means of the synchronous data-flow programming language lustre. IEEE Transactions on Software Engineering (1992); Special Issue on the Specification and Analysis of Real-Time Systems
Ressouche, A., Tigli, J.-Y., Oscar, C.: Composition and Formal Validation in Reactive Adaptive Middleware. Research report, PULSAR - INRIA Sophia Antipolis - INRIA - Laboratoire d’Informatique, Signaux, et Systèmes de Sophia-Antipolis (I3S) / Equipe RAINBOW - Université de Nice Sophia-Antipolis - CNRS: UMR6070, 02 (2011), Available from: http://hal.inria.fr/inria-00565860/en/
Satyanarayanan, M.: Fundamental challenges in mobile computing. In: Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, PODC 1996, pp. 1–7. ACM, New York (1996), http://doi.acm.org/10.1145/248052.248053 http://doi.acm.org/10.1145/248052.248053
Tigli, J.-Y., Lavirotte, S., Rey, G., Hourdin, V., Cheung, D., Callegari, E., Riveill, M.: Wcomp middleware for ubiquitous computing: Aspects and composite event-based web services. In: Annals of Telecommunication, vol. 6, Springer, Paris (2009) ; ISSN 0003-4347 (Print) 1958-9395 (Online)
Venkatasubramanian, N., Talcott, C., Agha, G.A.: A formal model for reasoning about adaptive qos-enabled middleware. ACM Trans. Softw. Eng. Methodol. 13(1), 86–147 (2004), http://doi.acm.org/10.1145/1005561.1005564 http://dx.doi.org/http://doi.acm.org/10.1145/1005561.1005564
Weiser, M.: The computer for the twenty-first century. Scientific American Ubicomp Paper 265, 94–104 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ressouche, A., Tigli, JY., Carrillo, O. (2011). Toward Validated Composition in Component-Based Adaptive Middleware. In: Apel, S., Jackson, E. (eds) Software Composition. SC 2011. Lecture Notes in Computer Science, vol 6708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22045-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-22045-6_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22044-9
Online ISBN: 978-3-642-22045-6
eBook Packages: Computer ScienceComputer Science (R0)