An Event-B Approach to Data Sharing Agreements

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. Key words: Data Sharing Agreements; Formal Analysis; Event-B

• Type: Journal
• Year: 2010
• Where: IFM
• Authors: Alvaro E. Arenas, Benjamin Aziz, Juan Bicarregui, Michael D. Wilson
• Keywords: Data Sharing Agreement, Deontic Notions, Event-B Specification Language, Formal Methods, IFM 2010