Ressources dynamiques: séparation et mise à jour – DynRes

La société attend des systèmes informatiques qu'ils soient corrects
et afin de maîtriser la complexité et l'hétérogénéité de ces systèmes,
il est nécessaire de mettre en place des cadres formels qui intégrent
des modèles différents, évoluant parfois dans des environnements
physiques distincts.
Dans ce contexte, un problème important lié à l'hétérogéneité est la
définition d'opérateurs de composition qui soient suffisamment
génériques pour être appliqués à de larges domaines tout en préservant
une sémantique cohérente pour les entités composées. Par ailleurs, il
y a une nécessité de développer des cadres théoriques qui permettent
l'intégration de composants et cela de façon cohérente sémantiquement.
Un formalisme logique standard pour exprimer des propriétés locales
sur la mémoire est la logique de séparation (SL) qui permet de
raisonner sur des structures de données dynamiques. En effet, SL peut
exprimer des propriétés sur des parties distinctes de la mémoire, et
cela à l'aide d'opérateurs dits de séparation. D'un point de vue
strictement sémantique, les modèles de SL sont très liés à la
modélisation d'états mémoires et SL peut exprimer et prouver des
propriétés essentielles sur des programmes qui manipulent des données
dynamiques. Toutefois cette logique souffre de quelques limitations:
elle a pour modèle une représentation concrète des états mémoire et
est de fait un language de spécification mais qui ne traite que d'une
une classe spécifique de modèles. De plus les propriétés liées aux
ressources exprimées par SL sont statiques et ne tiennent pas compte
de leur dynamique et la théorie de la preuve pour SL et ses variantes
n'en est qu'à ses balbutiements.

Il existe des logiques et modèles de ressources, issus de SL, qui sont
fondés sur des structures particulières, comme différentes sortes
d'arbres et de graphes. Ils se distinguent de SL par des axiomes
particuliers pour la séparation et proposent des structures ad-hoc
capturant un aspect spécifique de la composition de ressources. Il
existe des tentatives pour traiter de la mise à jour mais de façon
ad-hoc par rapport aux structures et donc avec des limitations dans le
contexte de la spécification et de la vérification. Ainsi on va ici
considérer les logiques de mise à jour, récemment étudiées pour
modéliser des structures de données et leur évolution, et chercher
à les développer pour traiter de la séparation et des resources
dynamiques.

Dans ce projet, l'objectif majeur consiste à établir les fondements de
nouveaux modèles de ressources, des formalismes logiques associés qui
traitent à la fois de la séparation et de la mise à jour.
Ainsi, notre but est d'étudier de nouveaux modèles de ressources ainsi
que des logiques pour la séparation et la mise à jour, qui soient
dédiées à la spécification et pour lesquelles la génération de preuves
ou de réfutations puissent être effectives. Cela correspond à une
étude sur les fondements mêmes des notions de séparation et de
mises à jour qui conduisent à deux directions de recherche non
explorées à ce jour: la spécification de systèmes et de propriétés de
ressources et de leur vérification à partir de la construction de
preuves et de réfutations. Les concepts de séparation et de mises à
jour ont été illustrés récemment dans d'autres formalismes pour
traiter des applications liées à la mémoire, et aux permissions par
exemple. Une analyse rapide de ces logiques détecte qu'elles ne sont
pas adaptées pour traiter des aspects dynamiques des ressources. Un
point essentiel du projet repose sur l'étude la combinaison des
aspects statiques et dynamiques des ressources. Ces considérations
sont au coeur des travaux de recherche des partenaires LORIA, LSV et
IRIT qui possèdent des experts en logiques temporelles, vérification
formelle, en modèles d'interaction et en démonstration automatique
pour logiques modales.