Extensions modales des logiques de ressources : expressivité et calculs

The design of new logical formalisms is at the heart of several problems in formal methods. Those formalisms must respond to requirements both concerning modelling (they must be able to describe certain systems) and computing (they must provide complete and sound calculus methods). In this context, we look at resource logics, and in particular BI and BBI logics, that deal with the separation and sharing of resources and have led to several separation logics whose applications to software verification have been widely developped recently. We propose in this thesis, starting from BI and BBI logics, to study some modal and epistemic separation logics by focusing on their modelling capacities and their expresiveness, as well as on the new proof calculi for those logics. A first study deals with the modelling of dynamic resource properties through new logic LTBI, which is a temporal separation logic, based on BI logic and temporal modalities. This logic notably offers interesting perspectives in temporal branching modelling, allowing for instance to characterize multi-thread processes. A complementary study concerns the modelling of access by agents to properties under the conditions of posessing some resources, through a new logic ERL, which is an epistemic separation logic, based on BBI logic and epistemic modalities. This logic allows many modellings of access control systems. In order to extend the expressivity of such separation logics, like BBI logic and its variants, a study on the internalization of resources symbols in the logic’s syntax has been developed through the new logics HRL and HBBI (hybrid version of BBI). Internalization allows both the extension of the expressivity of logics and the axiomatisation of BBI logic and some of its variants. In addition to the conception of those logics, the study of their semantics and their modelling capacities, a part of this thesis is dedicated to the definition of proof calculs, here tableaux calculus, for those new logics, as well as their proof of soundness and completenessLe développement de nouveaux formalismes logiques est au cœur de nombreuses problématiques de méthodes formelles. Ces formalismes doivent répondre à la fois à des impératifs de modélisation (ils doivent permettre de décrire certains systèmes) et de calcul (ils doivent fournir des méthodes de calcul correctes et complètes). Dans ce contexte, nous nous intéressons aux logiques de ressources, en particulier les logiques BI et BBI qui traitent du partage et de la séparation de ressources et qui ont conduit aux diverses logiques de séparation dont les applications à la vérification de programmes se sont développées fortement ces dernières années. Nous proposons dans cette thèse d’étudier, à partir des logiques BI et BBI, des logiques de séparation modales et épistémiques en se focalisant sur leurs capacités de modélisation et leur expressivité mais aussi les nouveaux calculs de preuve pour ces logiques. Une première étude a porté sur la modélisation de propriétés dynamiques de ressources au travers d’une nouvelle logique LTBI, qui est une logique de séparation temporelle, fondée sur la logique BI et des modalités temporelles. Cette logique offre notamment des perspectives intéressantes de modélisation temporelle branchante, permettant par exemple de caractériser les processus multi-thread. Une étude complémentaire a porté sur la modélisation de l’accès par des agents à des propriétés sous conditions de posséder certaines ressources, au travers d’une nouvelle logique ERL, qui est une logique de séparation épistémique, fondée sur la logique BBI et des modalités épistémiques. Cette logique permet de nombreuses modélisations de systèmes de contrôle d’accès. En vue d’étendre l’expressivité de telles logiques de séparation, comme la logique BBI et ses variantes, une étude sur l’internalisation des symboles de ressources dans la syntaxe de la logique a été développée au travers des nouvelles logiques HRL et HBBI (version hybride de BBI). L’internalisation permet à la fois d’étendre l’expressivité des logiques et d’axiomatiser la logique BBI et certaines de ses variantes. Outre la conception de ces logiques, l’étude de leur sémantique et aussi de leurs capacités de modélisation, une partie de cette thèse a été consacrée à la définition de calculs de preuve, ici de tableaux, pour ces nouvelles logiques ainsi qu’à leurs preuves de correction et de complétud