Collaboration inter-laboratoires entre le LIP et le LIRIS.
|
|
Projet soutenu par la Fédération Informatique de Lyon (en 2018-2020).
Collaboration inter-laboratoires entre le LIP et le LIRIS. |
Dans le contexte de l'internet des objets, on cherche à spécifier des objets connectés ayant des ressources consommables et limitées, et à les assembler de manière valide. Dans ce but on peut utiliser la logique linéaire pour décrire et certifier les cycles de vie de ces objets.
L'objectif est de tirer profit de la richesse d'expressivité de la logique linéaire pour décrire au mieux le comportement des objets et de s'appuyer sur la recherche automatique de preuve pour construire des assemblages d'objets, puis de les certifier dans le logiciel Coq à l'aide d'une librairie adaptée.