Abstract
We address the problem of automatically identifying what local properties the agents of a Cyber Physical System have to satisfy to guarantee a global required property \(\phi \). To enrich the picture, we consider properties where, besides qualitative requirements on the actions to be performed, we assume a weight associated with them: quantitative properties are specified through a weighted modal-logic. We propose both a formal machinery based on a Quantitative Partial Model Checking function on contexts, and a run-time machinery that algorithmically tries to check if the local behaviours proposed by the agents satisfy \(\phi \). The proposed approach can be seen as a run-time decomposition, privacy-sensitive in the sense agents do not have to disclose their full behaviour.
Research supported by: “VisColla” funded by Fondazione Cassa di Risparmio di Perugia; “BitCoins” co-funded by Banca d’Italia and Cassa di Risparmio di Perugia; the H2020 EU-funded European Network for Cyber Security, NeCS, (GA #675320).
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
Similar content being viewed by others
Notes
- 1.
Boolean c-semirings can be used to model crisp problems.
- 2.
\({\mathbb {K}}\) is complete if it is closed with respect to infinite sums, and the distributivity law holds also for an infinite number of summands [1].
- 3.
For the sake of readability, we write \(\Vert \) in place of \(\Vert ^2\), i.e., omitting the apex.
References
Bistarelli, S., Gadducci, F.: Enhancing constraints manipulation in semiring-based formalisms. In: ECAI, pp. 63–67 (2006)
Bistarelli, S., Montanari, U., Rossi, F.: Semiring-based constraint satisfaction and optimization. J. ACM 44(2), 201–236 (1997)
Bistarelli, S., Santini, F., Martinelli, F., Matteucci, I.: Automated adaptation via quantitative partial model checking. In: Proceedings of the 31st Annual ACM Symposium on Applied Computing, pp. 1993–1996. ACM (2016)
Blyth, T.S., Janowitz, M.E.: Residuation Theory, vol. 102. Pergamon press, Oxford (1972)
Buchholz, P., Kemper, P.: Quantifying the dynamic behavior of process algebras. In: Alfaro, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 184–199. Springer, Heidelberg (2001). doi:10.1007/3-540-44804-7_12
Cansado, A., Canal, C., Salaün, G., Cubo, J.: A formal framework for structural reconfiguration of components under behavioural adaptation. Electr. Notes Theor. Comput. Sci. 263, 95–110 (2010)
Derler, P., Lee, E.A., Sangiovanni-Vincentelli, A.L.: Modeling cyber-physical systems. Proc. IEEE 100(1), 13–28 (2012)
Gadducci, F., Hölzl, M., Monreale, G.V., Wirsing, M.: Soft constraints for lexicographic orders. In: Castro, F., Gelbukh, A., González, M. (eds.) MICAI 2013. LNCS (LNAI), vol. 8265, pp. 68–79. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45114-0_6
Gardelli, L., Viroli, M., Omicini, A.: Design patterns for self-organising systems. In: Burkhard, H.-D., Lindemann, G., Verbrugge, R., Varga, L.Z. (eds.) CEEMAS 2007. LNCS (LNAI), vol. 4696, pp. 123–132. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75254-7_13
Golan, J.: Semirings and Affine Equations Over Them: Theory and Applications. Kluwer Academic Publisher, Dordrecht (2003)
Larsen, K.G., Xinxin, L.: Compositionality through an operational semantics of contexts. J. Logic Comput. 1(6), 761–795 (1991)
Li, J., Yarvis, M., Reiher, P.: Securing distributed adaptation. Comput. Netw. 38(3), 347–371 (2002)
Lluch-Lafuente, A., Montanari, U.: Quantitative mu-calculus and CTL defined over constraint semirings. TCS 346(1), 135–160 (2005)
Martín, J.A., Martinelli, F., Pimentel, E.: Synthesis of secure adaptors. J. Log. Algebr. Program. 81(2), 99–126 (2012)
Martinelli, F., Matteucci, I., Santini, F.: Semiring-based specification approaches for quantitative security. In: Proceedings Thirteenth Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL. EPTCS, vol. 194, pp. 95–109 (2015)
Morandini, M., Penserini, L., Perini, A.: Towards goal-oriented development of self-adaptive systems. In: Workshop on Software Engineering for Adaptive and Self-managing Systems, SEAMS 2008, pp. 9–16. ACM (2008)
Shi, J., Wan, J., Yan, H., Suo, H.: A survey of cyber-physical systems. In: 2011 International Conference on Wireless Communications & Signal Processing, WCSP 2011, pp. 1–6. IEEE (2011)
Splunter, S., Wijngaards, N.J.E., Brazier, F.M.T.: Structuring agents for adaptation. In: Alonso, E., Kudenko, D., Kazakov, D. (eds.) AAMAS 2001-2002. LNCS (LNAI), vol. 2636, pp. 174–186. Springer, Heidelberg (2003). doi:10.1007/3-540-44826-8_11
Talcott, C., Arbab, F., Yadav, M.: Soft agents: exploring soft constraints to model robust adaptive distributed cyber-physical agent systems. In: Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 273–290. Springer, Cham (2015). doi:10.1007/978-3-319-15545-6_18
Viganò, L.: Automated security protocol analysis with the AVISPA tool. ENTCS 155, 69–86 (2006)
Wolf, T., Holvoet, T.: Design patterns for decentralised coordination in self-organising emergent systems. In: Brueckner, S.A., Hassas, S., Jelasity, M., Yamins, D. (eds.) ESOA 2006. LNCS (LNAI), vol. 4335, pp. 28–49. Springer, Heidelberg (2007). doi:10.1007/978-3-540-69868-5_3
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Bistarelli, S., Martinelli, F., Matteucci, I., Santini, F. (2017). A Formal and Run-Time Framework for the Adaptation of Local Behaviours to Match a Global Property. In: Kouchnarenko, O., Khosravi, R. (eds) Formal Aspects of Component Software. FACS 2016. Lecture Notes in Computer Science(), vol 10231. Springer, Cham. https://doi.org/10.1007/978-3-319-57666-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-57666-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57665-7
Online ISBN: 978-3-319-57666-4
eBook Packages: Computer ScienceComputer Science (R0)