[Back]

C. Tsigkanos:
"Towards Dependable Internet-of-Things: Situating Control, Data and Verification close to end-devices";
Talk: National Institute of Informatics (NII), Invitation by Prof. Zhenjiang Hu, Tokyo, Japan (invited); 2019-03-18.

Contemporary Internet of Things (IoT) systems are dynamic, without stable spatial and temporal boundaries, and involve mostly independent software components. IoT systems provide data-centric, device-centric and service-centric functionalities that are subject to continuous disruption, under limitations such as resource-constrained devices, platforms heterogeneity, and deployment in adverse environments or administrative domains. As these systems evolve and gain complexity, their dependability becomes a crucial system property. This entails understanding and systematically managing dynamic behavior and decentralizing operations, and requires a paradigm shift; marrying distributed systems and formal aspects of software engineering. In this talk, we will discuss three representative aspects of engineering dependable IoT systems: situating control, data management, and verification logic close to IoT end-devices.
i) Since resources within the IoT are often distributed among participating devices, coordination is required to utilize resources for achieving their goals. Moreover, this must occur in the absence of central control. To this end, we will discuss bounded model checking to compute resource coordination plans opportunistically at runtime and on low-powered devices. Plans are computed without any knowledge about the operational status of the IoT system or which resources are present at the system's design time.
ii) The role of data is certainly an integral part of the IoT - particularly how data flows between components that comprise the IoT system. Motivated by the "Data protection by design and by default" discipline, we will discuss a technical framework to support privacy-aware data synchronization among components tailored for pervasive IoT applications. Synchronization is based on the P-RBAC privacy model and able to capture roles and permissions, actions on data, conditions and obligations that arise in requirements. For automated and correct reflection of synchronized data among components, bidirectional transformations are adopted, guaranteeing consistency and well-behavedness.
iii) IoT systems are often spatially-distributed, and this distribution can be crucial to requirements satisfaction. Formal verification techniques need to be in place while systems operate to ensure that requirements are fulfilled. This may be achieved by keeping a model of the system at runtime, monitoring events that lead to changes, and performing analysis. Analysis entails model checking of requirements expressed in a spatial logic; this computationally-intensive runtime assurance method cannot be supported by resource-constrained devices and must be offloaded to the cloud. There, challenges arise regarding resource allocation and cost, especially when the workload is unknown at design time. As such, it may be difficult to guarantee application service level agreements, e.g., on response times. We will discuss how spatial verification processes can be integrated in the service layer of an IoT-cloud architecture based on microservices, and assess their tradeoffs across different deployment options.