An Event-B approach to data sharing agreements

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

An Event-B approach to data sharing agreements

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

School of Computing

Research output: Contribution to conference › Paper › peer-review

131 Downloads (Pure)

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 speciﬁcation 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 language	English
Publication status	Published - 11 Oct 2010
Event	8th International Conference on Integrated Formal Methods - Nancy, France Duration: 11 Oct 2010 → 14 Oct 2010

Conference

Conference	8th International Conference on Integrated Formal Methods
Abbreviated title	iFM 2010
Country/Territory	France
City	Nancy
Period	11/10/10 → 14/10/10

Keywords

Data Sharing Agreements
Formal Analysis
Event-B

Access to Document

DSA-EventB.pdfAccepted author manuscript (Post-print), 345 KB

http://www.springerlink.com/content/lw1758473ng2t065/

Cite this

@conference{03d61f66b07843d3a7be4f6012fe36ae,

title = "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 speciﬁcation 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{\textquoteright} actions are in agreement with the DSA clauses.",

keywords = "Data Sharing Agreements, Formal Analysis, Event-B",

author = "A. Arenas and Benjamin Aziz and J. Bicarregui and M. Wilson",

note = "Projects: Security and Forensics.; 8th International Conference on Integrated Formal Methods, iFM 2010 ; Conference date: 11-10-2010 Through 14-10-2010",

year = "2010",

month = oct,

day = "11",

language = "English",

}

TY - CONF

T1 - An Event-B approach to data sharing agreements

AU - Arenas, A.

AU - Aziz, Benjamin

AU - Bicarregui, J.

AU - Wilson, M.

N1 - Projects: Security and Forensics.

PY - 2010/10/11

Y1 - 2010/10/11

N2 - 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 speciﬁcation 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.

AB - 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 speciﬁcation 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.

KW - Data Sharing Agreements

KW - Formal Analysis

KW - Event-B

M3 - Paper

T2 - 8th International Conference on Integrated Formal Methods

Y2 - 11 October 2010 through 14 October 2010

ER -

An Event-B approach to data sharing agreements

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this