The aim of the proposed project is to develop new software technologies to enable (self-)adaptivity of IoT systems while reinforcing the safety of their operation. The obtained results will be applied and evaluated in the context of a real industrial IoT system designed for tracking and management of equipment parks.
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.
The proposed solution comprises three key elements:
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.
Proposed research project
Operation of low-cost off-the-shelf devices, which are often used in IoT systems, is subject to several sources of faults, e.g. battery depletion, interference, or shadowing. A typical difficulty in the context of the IoT systems developed by Charlie Solutions, arises when two vehicles or containers a positioned closed to each other: the corresponding gateways may detect the equipment in both locations, sending conflicting signals to the platform.
In general, low-level connectivity faults affect the reliability of the collected data. They also propagate to higher levels of abstraction. For instance, they induce variations on the network topology, e.g. when a key retransmitting device becomes temporarily or permanently unavailable.
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 , adopting the Rigorous System Design approach , whereby the design proceeds as follows :
A set of user requirements is formulated in a pseudo-natural Domain-Specific Language (DSL) and translated into formally defined behavioural properties.
For each formal property a corresponding design pattern (architecture ) is identified and applied to the model.
The model is analysed to ensure consistency and satisfaction of additional properties, which cannot be enforced by architectures.
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:
characterise the application domain (system actors, event types, constraints, potential problems)
design and implement a software infrastructure allowing the coordination of the dynamic behaviour of system components
define a DSL for describing the coordination policies
develop methods and tools for the consistency analysis of user-defined policies
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.
- Master transcript
- Coordinates for 1-2 persons that can recommend you
- Ananda Basu, Saddek Bensalem, Marius Bozga, Jacques Combaz, Mohamad Jaber, Thanh-Hung Nguyen, Joseph Sifakis: Rigorous component-based system design using the BIP framework. IEEE Software 28(3) (2011) 41–48 [PDF]
- Joseph Sifakis: Rigorous System Design. Foundations and Trends® in Electronic Design Automation 6(4) (2012) 293–362 [PDF]
- Emmanouela Stachtiari, Anastasia Mavridou, Panagiotis Katsaros, Simon Bliudze, and Joseph Sifakis: Early validation of system requirements and design through correctness-by-construction. Journal of Systems and Software 145 (2018) 52–78 [PDF]
- Paul Attie, Eduard Baranov, Simon Bliudze, Mohamad Jaber, Joseph Sifakis: A general framework for architecture composability. Formal Aspects of Computing 18(2) (2016) 207–231 [Open Access]