Formal methods for exchange policy specification

We focus on information control within information systems in the context of shared governance to deal with crises. By crises, we mean, problems like disease surveillance, syndromic surveillance, Earth observation (for monitoring and management of natural disasters), space observation (like space situational awareness), but also the dissemination of information to the public such as pollution alerts or incident alerts. All these problems have become global and require a coordinated response. It has indeed become unrealistic to think that a single actor could answer alone.

However, States, agencies, firms, companies and organizations do not communicate openly and without constraint. Upstream of the realization of any system, we need a framework to express the ins and outs related to the exchange and the dissemination of information. This framework allows us to formally prove that the system filled well its alerts missions while ensuring the control of information and thus, ultimately, build the trust amongst the different partners.


Articles available on demand (email me)

  • Rémi Delmas and Thomas Polacsek. Need-to-share & non-diffusion requirements verification in exchange policies 27th International Conference on Advanced Information Systems Engineering (CAISE'15), 2015.
    Abstract: Whether be it for Earth observation, risk management or even companies relations, more and more interconnected organizations form decentralized systems in which the exchange, in terms of diffusion or non-diffusion of information between agents, can have critical consequences.
    In this paper, we present a formal framework to specify information exchange policies for such kinds of systems and two specific requirements, the need-to-share and the non-diffusion requirements, as well as properties strongly related to them. Wiser from these formal definitions, we see how to reconcile these sometimes two antagonist requirements in a same policy specification with information filtering operations. We also explain how we use state of the art theorem provers to perform automatic analysis of these policies.
  • Rémi Delmas et Thomas Polacsek. Critical Information Diffusion Systems. Wisard ADBIS 2015 workshop, 2015.
  • Rémi Delmas and Thomas Polacsek. Formal methods for exchange policy specification. 25th International Conference on Advanced Information Systems Engineering (CAISE'2013), 2013
    Abstract: This paper introduces a modelling framework to perform automatic analyses on the specification of an information exchange policy. To avoid the increase of development costs and risks of uncontrolled dissemination of information, the specification errors need to be detected before the implementation phase. We propose a minimalistic core language to unambiguously represent an exchange policy specification and a gateway to logic solvers to verify some properties, namely: completeness, consistency, applicability and minimality. The aim is to check wether the formalisation of an exchange policy is consistent with user expectations.