HARVEY: On Runtime Verifcation of Cyber-Physical Spaces

Cyber-physical spaces are complex environments with embedded computing and communi- cation 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. caused by the complexity of the system or a 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 definition of a runtime verification technical framework able to mon- itor behavioral properties of cyber-physical spaces. Cyber-physical 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, cap- turing 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.We realize our online monitoring approach as HARVEY, a lightweight framework for monitoring complex formulae expressed in MFTOL over parametric bigraphs, where for the evaluation of MFOTL predicates and bigraphical patterns, external tools are integrated. The evaluation of our framework passes through a case study of a bike sharing system in a smart city, and discuss preliminary results regarding expressiveness of our approach.