An Event-B Approach to Data Sharing Agreements

Abstract : 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.
Type de document :
Communication dans un congrès
Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.28-42, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00525098
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : lundi 11 octobre 2010 - 11:14:46
Dernière modification le : lundi 11 octobre 2010 - 11:14:46

Identifiants

  • HAL Id : inria-00525098, version 1

Collections

Citation

Alvaro E. Arenas, Benjamin Aziz, Juan Bicarregui, Michael D. Wilson. An Event-B Approach to Data Sharing Agreements. Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.28-42, 2010, Lecture Notes in Computer Science. 〈inria-00525098〉

Partager

Métriques

Consultations de la notice

36