The presentation concerns a model-based approach to developing robotic system controllers. Central to this approach is a parameterised meta-model that describes the generic robotic system from two points of view: structure and activity. By appropriate parametrisation of the meta-model one can obtain a particular model of a robotic system performing desired tasks. The meta-model is expressed using the Robotic System Hierarchical Petri Net (RSHPN), a 6-layer Petri net tailored for robotics. Each layer describes the activity of the robotic system at a completely different level of abstraction. This guarantees the separation of concerns. The required model emerges from the meta-model by appropriate parametrisation of the layers of the RSHPN. Introduction of parametrisation enables the robot designer to focus only on the concepts derived from the domain. It greatly facilitates the robotic system development process as it gives the designer clear guidance on what needs to be defined and what is imposed by the design pattern. The resulting single RSHPN model is used both to verify some properties of the system, e.g. lack of deadlocks, but also to automatically generate controller code. The presented approach is illustrated by examples of the creation of two different robotic systems.
Séminaires SCALP
Les spécifications basées sur les schémas-blocs et machines à états sont utilisées pour la conception de systèmes de contrôle-commande, particulièrement dans le développement d’applications critiques. Des outils tels que Scade et Simulink/Stateflow sont équipés de compilateurs qui traduisent de telles spécifications en code exécutable. Ils proposent des langages de programmation permettant de composer des fonctions sur des flots, tel que l’illustre le langage synchrone à flots de données Lustre.
Cet exposé présente Vélus, un compilateur Lustre vérifié dans l’assistant de preuves interactif Coq. Nous développons des modèles sémantiques pour les langages de la chaîne de compilation, et utilisons le compilateur C vérifié CompCert pour générer du code exécutable et donner une preuve de correction de bout en bout.
Le défi principal est de montrer la préservation de la sémantique entre le paradigme flots de données et le paradigme impératif, et de raisonner sur la représentation bas niveau de l’état d’un programme. En particulier, nous traitons le reset modulaire, une primitive pour réinitialiser des sous-systèmes. Ceci implique la mise en place de modèles sémantiques adéquats, d’algorithmes de compilation et des preuves de correction correspondantes.
Dans un second temps, une autre approche de la compilation vérifiée est présentée dans le cadre d'un travail de recherche actuel sur le compilateur LustreC. Ce travail consiste à transformer LustreC en compilateur certifiant, qui génère du code et de la spécification associée prouvée a posteriori par des outils comme Frama-C ou SPARK.
Vidéo disponible ici : https://prismes.univ-toulouse.fr/player.php?code=70Bn133d&width=100%&height=100%
Ce séminaire sera consacré à la présentation d'une formule d'évaluation des enchères pour la résolution du problème d'allocation de tâches aux systèmes multi-robots. Notre contribution se focalise sur l'amélioration des communications entre les robots, grâce à la proposition d'un terme spécialisé inclus dans l'évaluation des enchères. Notre méthode a été évaluée dans un scénario de patrouille grâce à des simulations numériques. Ces évaluations démontrent que la préservation des communications améliore la robustesse du système multi-robots, lorsqu'ils sont sujets à des pannes.
Vidéo disponible ici : https://prismes.univ-toulouse.fr/player.php?code=166463Tj&width=100%&height=100%