Task planning under constraints

The autonomy of embedded systems, in particular robots, comes from their capability to plan their next actions. Although, it becomes critical to ensure the safety of the behaviour as the systems are exposed to human interaction more and more (eg. Autonomous cars, toy UAVs, cobots in manufacturing and so on).
The goal of the thesis is to study task planning under constraints: select the best sequence of actions while optimising several criteria like efficiency, safety and other domain specifics. The thesis involves two main axes, the first is to study how to model the systems constraints in a manner that can be understood both by the human experts and the planning algorithm (eg. Using Operational Design Domain or Dynamic Assurance Case to evaluate system’s safety). Ontologies and knowledge graphs would probably be adequate to model the constraints. The model would benefit from their expressivity and the already-existing tooling. The second main axis is the improvement of the planning algorithm to leverage those models. Those models shall have a generic structure since it is necessary to represent many natures of constraints: safety, efficiency/cost, social “confort”, shared resources on the critical path, type and quantity of interactions between the agents, geometric feasibility, ...
As the thesis is aimed at robotic autonomous systems, it will be important to demonstrate and evaluate the system on real-world use cases.

A formal framework for the specification and verification of distributed processes communication flows in clouds

Clouds are constituted of servers interconnected via the Internet, on which systems can be implemented, making use of applications and databases deployed on the servers. Cloud-based computing is gaining in popularity, and that includes the context of critical systems. As a result, it is useful to define formal frameworks for reasoning about cloud-based systems. One requirement about such a framework is that it enables reasoning about the concepts manipulated in a cloud, which naturally includes the ability to reason about distributed systems, composed of subsystems deployed on different machines and interacting through message passing to implement services. In this context, the ability to reason about communication flows is central. The aim of this thesis is to define a formal framework dedicated to the specification and verification of systems deployed on clouds. This framework will capitalize on the formal framework of "interactions". Interactions are models dedicated to the specification of communication flows between different actors in a system. The thesis work will study how to define structuring (enrichment, composition) and refinement operators to enable the implementation of classical software engineering processes based on interactions.

Top