IIT Home Page CNR Home Page

A Formal and Run-time Framework for the Adaptation of Local Behaviours to Match a Global Property

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 . 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 specied 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 . 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.


Formal Aspects of Component Software - The 13th International Conference, Besançon, France, 2016

External authors: Stefano Bistarelli (Dipartimento di Matematica e Informatica, University of Perugia, Italy), Francesco Santini (Dipartimento di Matematica e Informatica, University of Perugia, Italy)
IIT authors:

Type: Contributo in atti di convegno
Field of reference: Information Technology and Communication Systems

File: main.pdf

Activity: Architetture, protocolli e meccanismi di sicurezza per sistemi e servizi distribuiti