An Event-B approach to data sharing agreements

A. Arenas, Benjamin Aziz, J. Bicarregui, M. Wilson

Research output: Contribution to conferencePaperpeer-review

121 Downloads (Pure)


A Data Sharing Agreement (DSA) is a contract among two or more principals regulating how they share data. Agreements are usually represented as a set of clauses expressed using the deontic notions of obligation, prohibition and permission. In this paper, we present how to model DSAs using the Event-B specification language. Agreement clauses are modelled as temporal-logic formulas that preserve the intuitive meaning of the deontic operators, and constrain the actions that a principal can execute. We have exploited the ProB animator and model checker in order to verify that a system behaves according to its associated DSA and to validate that principals’ actions are in agreement with the DSA clauses.
Original languageEnglish
Publication statusPublished - 11 Oct 2010
Event8th International Conference on Integrated Formal Methods - Nancy, France
Duration: 11 Oct 201014 Oct 2010


Conference8th International Conference on Integrated Formal Methods
Abbreviated titleiFM 2010


  • Data Sharing Agreements
  • Formal Analysis
  • Event-B


Dive into the research topics of 'An Event-B approach to data sharing agreements'. Together they form a unique fingerprint.

Cite this