HarVey. On runtime veri cation of cyber-physical spaces

Cyber-physical spaces are complex environments with embedded computing and communication capabilities, where there's no clear boundary between digital and physical world. Smart cities or smart buildings are common examples of cyber-physical spaces. In such systems, where integrated digital services are provided to users thanks to technologies like the Internet of Things or Cloud computing, we must guarantee that a service is delivered to a user in the intended way, avoiding undesired behaviors that may lead to requirement violations. Often, such behaviors cannot be ensured at design time, e.g. due to the complexity of the system or the high number of agents interacting with it. Thus, techniques situated at runtime to monitor a system's behavior must be considered, which usually enable stating properties of a system in a suitable formal language as well as ensuring that the system does not violate them. This thesis aims at the de nition of a runtime veri cation technical framework able to monitor behavioral properties of cyber-physical spaces. Cyberphysical spaces are modelled using bigraphs, a formalism for structures in ubiquitous computing, while properties are expressed using Metric First Order Temporal Logic (MFOTL) over parametric bigraphical patterns, capturing both structural and temporal properties of a system. The resulting language can be used to monitor complex cyber-physical environments such as smart cities or buildings. For the evaluation of MFOTL predicates and bigraphical patterns, external tools are integrated. We evaluate our framework using a case study of a bike sharing system in a smart city, and discuss preliminary results regarding expressiveness and realizability of our approach.

Gli spazi cyber-fisici sono ambienti complessi, con capacità di calcolo e comunicazione integrate, dove non c'è un chiaro confine tra il mondo digitale e quello fisico. Le smart cities o gli smart buildings sono un classico esempio di spazi cyber-physici. In questi sistemi, dove agli utenti vengono forniti servizi digitali grazie a tecnologie come l'Internet of Things o il Cloud computing, è necessario garantire che il servizio sia effettivamente erogato nella maniera prestabilita, evitando comportamenti indesiderati che potrebbero portare ad una violazione dei requisiti del sistema stesso. Spesso, questi comportamenti non possono essere verificati in fase di design del sistema, per esempio per via della complessità del sistema stesso o l'elevato numero di agenti che interagiscono con esso. Servono perciò delle tecniche applicate in fase di esecuzione del sistema per monitorarne il comportamento, che solitamente consentono di esprimere proprietà del sistema in uno specifico linguaggio formale, oltre che assicurare che il sistema non violi tali proprietà. Questa tesi ha come obiettivo la definizione di un framework per la verifica a runtime di uno spazio cyber-fisico, in grado di monitorarne propriet\'{a} comportamentali. Gli spazi cyber-physici sono modellizzati attraverso l'uso di grafi bipartiti, mentre le propriet\'{a} sono espresse in logica temporale metrica del primo ordine (MFOTL), che usando grafi bipartiti al suo interno consente di descrivere sia propriet\'{a} strutturali che propriet\'{a} temporali. Il linguaggio risultante pu\`{o} essere usato per monitorare ambienti cyber-fisici complessi, come smart cities o smart buildings. Per la valutazione dei predicati logici e dei grafi bipartiti, sono stati integrati componenti aggiuntivi. Il framework \`{e} stato valutato usando come caso di studio un systema di bike sharing in una smart city, discutendo l'espressivit\'{a} e la realizzabilit\'{a} del nostro approccio.