Abstract
Self-adaptation allows systems to modify their structure and/or their behaviour depending on the environment and the system itself. Since reconfigurations must not happen at any but in suitable circumstances, guiding and controlling dynamic reconfigurations at runtime is an important issue. This paper contributes to two essential topics of the self-adaptation—a runtime temporal properties evaluation, and a decentralization of control loops. It extends the work on the adaptation of component-based systems at runtime via policies with temporal patterns by providings (a) specific progressive semantics of temporal patterns and (b) a decentralised method which is suitable to deal with temporal patterns of component-based systems at runtime. The implementation with the GROOVE tool constitutes a practical contribution.
This work has been partially funded by the Labex ACTION, ANR-11-LABX-0001-01.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
By definition in [16], this conjunction is in \(CP\).
- 2.
FTPL stands for TPL (Temporal Pattern Language) prefixed by ‘F’ to denote its relation to Fractal-like components and to first-order integrity constraints over them.
- 3.
Implemented as controllers in CSP\(\Vert \)B, Fractal, FraSCAti, etc.
- 4.
For relations involving two components (like Delegate or Parent) we consider that only the parent component is aware of the relation. For the Binding relation, only the component owning the required (or client) interface is aware of the binding.
- 5.
wrt. the semantics.
- 6.
In the case where there are two or more equally urgent formulae, \(\varphi \) is sent to a monitor determined by an arbitrary order with the function \(Mon:\mathcal {M} \times 2^{AE} \rightarrow \mathcal {M}\). \(Mon(M_i,AE^\prime )=M_{j_{min}}\) s.t \(j_{min} = min(j \in [1,n] \backslash \{i\} | AE^\prime \cap AE_j \not = \varnothing )\).
- 7.
The formula to evaluate as well as its sub-formulae evaluated at the current state.
- 8.
This allows all monitors to keep a history of \(|\mathcal {M}|+1\) configurations.
References
de Lemos, R., et al.: Software engineering for self-adaptive systems: a second research roadmap. In: de Lemos, R., Giese, H., Müller, H.A., Shaw, M. (eds.) Software Engineering for Self-Adaptive Systems. LNCS, vol. 7475, pp. 1–32. Springer, Heidelberg (2013)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Software Engineering, pp. 411–420 (1999)
Kouchnarenko, O., Weber, J.-F.: Adapting component-based systems at runtime via policies with temporal patterns. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 234–253. Springer, Heidelberg (2014)
Bauer, A., Falcone, Y.: Decentralised LTL monitoring. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 85–100. Springer, Heidelberg (2012)
Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using GROOVE. Int. J. Softw. Tools Technol. Trans. 14, 15–40 (2012)
Kupferman, O., Vardi, M.Y., Wolper, P.: Module checking. Inf. Comput. 164, 322–344 (2001)
Bozzelli, L., Murano, A., Peron, A.: Pushdown module checking. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 504–518. Springer, Heidelberg (2005)
Aminof, B., Legay, A., Murano, A., Serre, O., Vardi, M.Y.: Pushdown module checking with imperfect information. Inf. Comput. 223, 1–17 (2013)
Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. Int. J. Logic Comput. 20, 651–674 (2010)
Kim, M., Lee, I., Shin, J., Sokolsky, O., et al.: Monitoring, checking, and steering of real-time systems. ENTCS 70, 95–111 (2002)
Bruneton, E., Coupaye, T., Leclercq, M., Quéma, V., Stefani, J.B.: The fractal component model and its support in java. Softw. Pract. Exper. 36, 1257–1284 (2006)
Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Formal Asp. Comput. 17, 390–422 (2005)
Seinturier, L., Merle, P., Rouvoy, R., Romero, D., Schiavoni, V., Stefani, J.B.: A component-based middleware platform for reconfigurable service-oriented architectures. Softw. Practice Experience 42, 559–583 (2012)
Garavel, H., Mateescu, R., Serwe, W.: Large-scale distributed verification using cadp: Beyond clusters to grids. Electr. Notes Theor. Comput. Sci. 296, 145–161 (2013)
Dormoy, J., Kouchnarenko, O., Lanoix, A.: Runtime verification of temporal patterns for dynamic reconfigurations of components. In: Arbab, F., Ölveczky, P.C. (eds.) FACS 2011. LNCS, vol. 7253, pp. 115–132. Springer, Heidelberg (2012)
Hamilton, A.G.: Logic for Mathematicians. Cambridge University Press, Cambridge (1978)
Dormoy, J., Kouchnarenko, O., Lanoix, A.: When structural refinement of components keeps temporal properties over reconfigurations. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 171–186. Springer, Heidelberg (2012)
Dormoy, J., Kouchnarenko, O., Lanoix, A.: Using temporal logic for dynamic reconfigurations of components. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS, vol. 6921, pp. 200–217. Springer, Heidelberg (2012)
Kouchnarenko, O., Weber, J.F.: Decentralised Evaluation of Temporal Patterns over Component-based Systems at Runtime (2014). Long version of the present paper available at: http://hal.archives-ouvertes.fr/hal-01044639
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Kouchnarenko, O., Weber, JF. (2015). Decentralised Evaluation of Temporal Patterns over Component-Based Systems at Runtime. In: Lanese, I., Madelaine, E. (eds) Formal Aspects of Component Software. FACS 2014. Lecture Notes in Computer Science(), vol 8997. Springer, Cham. https://doi.org/10.1007/978-3-319-15317-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-15317-9_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15316-2
Online ISBN: 978-3-319-15317-9
eBook Packages: Computer ScienceComputer Science (R0)