Coordination for Safe Adaptivity of IoT Systems

The term Internet of Things (IoT) designates the technology that relies on a large collection of distributed sensors to collect a broad variety of data. After a potential aggregation phase, these data are typically transferred to a cloud platform for processing, analysis and to be used for guiding decision-making processes. IoT popularity has grown dramatically in recent years, due to the progress in sensor technologies, leading to sensor miniaturisation and reduced life-cycle costs.

Although specific instances vary in size—from tens of devices in a smart-home system, through hundreds or thousands in industrial monitoring, all the way to hundreds of thousands projected for smart cities—even the smaller IoT systems give rise to significant complexity because of their inherently concurrent nature.

The PhD project is part of the collaboration between the Spirals team at Inria Lille – Nord Europe and Charlie Solutions—a young start-up based in Lille, specialising in the management and tracking of equipment parks using an innovative IoT solution for automated traceability combined with a Software as a Service (SaaS) platform and a mobile application.

• an active BLE sensor attached to each piece of the monitored equipement

• an active geolocalised gateway for each storage zone (container, vehicle, warehouse)

• a Software as a Service (SaaS) equipement management platform

The gateways receive and aggregate the signals emitted by the sensors and transmit them to the SaaS platform used to present the information to the user (manager responsible for the equipment park). Furthermore, the platform analyses the data and raises alerts attracting attention to any problematic situations. It can also propose appropriate corrective actions.

When an IoT sub-system is used to drive the control of a critical system, it is essential to ensure that it satisfy the appropriate safety properties (intuitively: "a given bad outcome will never happen") all while maintaining the system availability. The properties involved can be generic, e.g. "the sensing network is always connected", or domain-specific, e.g. "closing of the garage door is blocked whenever a running car engine is detected", defined respectively, by the environment and user constraints.

To provide safety guarantees in spite of the system complexity we will rely on the design of a formal framework for component-based modelling, analysis and generation of code for component-based IoT systems. This framework will extend the principles defined by BIP [1], adopting the Rigorous System Design approach [2], whereby the design proceeds as follows [3]:

1. A set of user requirements is formulated in a pseudo-natural Domain-Specific Language (DSL) and translated into formally defined behavioural properties.

2. For each formal property a corresponding design pattern (architecture [4]) is identified and applied to the model.

3. The model is analysed to ensure consistency and satisfaction of additional properties, which cannot be enforced by architectures.

4. Source code is automatically generated from the model for each component of the system as well as as the glue code for the coordination of their interactions.

The goal of this PhD project is to put in place a software framework for the design of safe IoT systems capable of adapting dynamically to the evolution of both the environment and of the user requirements.

To that end, the PhD student will be expected to make the following four contributions:

1. characterise the application domain (system actors, event types, constraints, potential problems)

2. design and implement a software infrastructure allowing the coordination of the dynamic behaviour of system components

3. define a DSL for describing the coordination policies

4. develop methods and tools for the consistency analysis of user-defined policies

The PhD project is financed through the CIFRE agreement involving Spirals and Charlie Solutions. Hence, the PhD student will be sharing their time among the two locations.

Spirals (Self-adaptation for distributed services and large software systems) is a project-team at the Inria Lille – Nord Europe research centre. Its research program focuses on defining self-adaptive distributed software services and systems. In particular, one of the two key properties that it targets is self-optimisation, i.e. the capability of systems to continuously reason about themselves and to take appropriate decisions and actions on the optimisations they can apply to improve their usage of the available resources. In order to provide this capability, Spirals is conducting a study of mechanisms for monitoring, taking decisions, and automatically reconfiguring software at run-time and at various scales.

Charlie Solutions is a young start-up based in Lille, specialising in the management and tracking of equipment parks using an innovative IoT solution for automated traceability combined with a Software as a Service (SaaS) platform and a mobile application. They aim at addressing, in particular, the problems of theft and loss of equipment, duplicate equipment, monitoring and ordering errors, encountered by any company with a large fleet of equipment deployed for multi-site outdoor operations. Targeting the construction, event and local authorities markets, Charlie Solutions allows their clients to reduce renewal and maintenance costs, better control deadlines and, thus, to optimize the profitability of their equipment fleets.

The following skills are required for this project:

• mathematical reasoning (be able to formally state and prove a reasonably complex mathematical result)
• basics of discrete mathematics (e.g. automata, predicate logics)
• proficiency in PHP
• proficiency in at least one of Python, C++, or Java
• fluent spoken and written English

The following skills are not required, but could constitute a plus:

• past experience with IoT systems
• past experience with requirement elicitation and/or business rules
• advanced knowledge of formal methods (e.g. temporal logics)

Please apply by e-mail to Simon Bliudze.
Applications will be processed as soon as they arrive.

Attach:

• CV
• Master transcript
• Coordinates for 1-2 persons that can recommend you