Checking Accountability with a Prover

Walid Benghabrit; Herve Grall; Jean Claude Royer; Mohamed Sellami

doi:10.1109/COMPSAC.2015.8

Checking Accountability with a Prover

Walid Benghabrit, Herve Grall, Jean Claude Royer, Mohamed Sellami

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Today on-line services are the cornerstone of on-line applications such as e-commerce, e-government and e-health applications. However, they raise several challenges about data privacy. Accountability, which is the property of an entity of being responsible for its acts, meets some of these challenges and hence increases user's trustworthiness in on-line applications. In this work, we propose an approach to assist the design of accountable applications. In particular, we consider an application's abstract component design and we introduce a logical approach allowing various static verifications. This approach offers effective means to early check the design and the behavior of an application and its offered/required services. We motivate our work with a realistic use case coming from the A4Cloud project and validate our proposal with experiments using a theorem prover.

Original language	English
Title of host publication	Proceedings - 2015 IEEE 39th Annual Computer Software and Applications Conference, COMPSAC 2015
Editors	Gang Huang, Jingwei Yang, Sheikh Iqbal Ahamed, Pao-Ann Hsiung, Carl K. Chang, William Chu, Ivica Crnkovic
Publisher	IEEE Computer Society
Pages	83-88
Number of pages	6
ISBN (Electronic)	9781467365635
DOIs	https://doi.org/10.1109/COMPSAC.2015.8
Publication status	Published - 21 Sept 2015
Externally published	Yes
Event	39th IEEE Annual Computer Software and Applications Conference, COMPSAC 2015 - Taichung, Taiwan, Province of China Duration: 1 Jul 2015 → 5 Jul 2015

Publication series

Name	Proceedings - International Computer Software and Applications Conference
Volume	2
ISSN (Print)	0730-3157

Conference

Conference	39th IEEE Annual Computer Software and Applications Conference, COMPSAC 2015
Country/Territory	Taiwan, Province of China
City	Taichung
Period	1/07/15 → 5/07/15

Keywords

Accountability language
Component diagram
First-order temporal logic
Prover
Software design
Verification

Access to Document

10.1109/COMPSAC.2015.8

Cite this

Benghabrit, W., Grall, H., Royer, J. C., & Sellami, M. (2015). Checking Accountability with a Prover. In G. Huang, J. Yang, S. I. Ahamed, P.-A. Hsiung, C. K. Chang, W. Chu, & I. Crnkovic (Eds.), Proceedings - 2015 IEEE 39th Annual Computer Software and Applications Conference, COMPSAC 2015 (pp. 83-88). Article 7273604 (Proceedings - International Computer Software and Applications Conference; Vol. 2). IEEE Computer Society. https://doi.org/10.1109/COMPSAC.2015.8

Benghabrit, Walid ; Grall, Herve ; Royer, Jean Claude et al. / Checking Accountability with a Prover. Proceedings - 2015 IEEE 39th Annual Computer Software and Applications Conference, COMPSAC 2015. editor / Gang Huang ; Jingwei Yang ; Sheikh Iqbal Ahamed ; Pao-Ann Hsiung ; Carl K. Chang ; William Chu ; Ivica Crnkovic. IEEE Computer Society, 2015. pp. 83-88 (Proceedings - International Computer Software and Applications Conference).

@inproceedings{ecfa805a0fef4bd0b6a57109304de3d5,

title = "Checking Accountability with a Prover",

abstract = "Today on-line services are the cornerstone of on-line applications such as e-commerce, e-government and e-health applications. However, they raise several challenges about data privacy. Accountability, which is the property of an entity of being responsible for its acts, meets some of these challenges and hence increases user's trustworthiness in on-line applications. In this work, we propose an approach to assist the design of accountable applications. In particular, we consider an application's abstract component design and we introduce a logical approach allowing various static verifications. This approach offers effective means to early check the design and the behavior of an application and its offered/required services. We motivate our work with a realistic use case coming from the A4Cloud project and validate our proposal with experiments using a theorem prover.",

keywords = "Accountability language, Component diagram, First-order temporal logic, Prover, Software design, Verification",

author = "Walid Benghabrit and Herve Grall and Royer, \{Jean Claude\} and Mohamed Sellami",

note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 39th IEEE Annual Computer Software and Applications Conference, COMPSAC 2015 ; Conference date: 01-07-2015 Through 05-07-2015",

year = "2015",

month = sep,

day = "21",

doi = "10.1109/COMPSAC.2015.8",

language = "English",

series = "Proceedings - International Computer Software and Applications Conference",

publisher = "IEEE Computer Society",

pages = "83--88",

editor = "Gang Huang and Jingwei Yang and Ahamed, \{Sheikh Iqbal\} and Pao-Ann Hsiung and Chang, \{Carl K.\} and William Chu and Ivica Crnkovic",

booktitle = "Proceedings - 2015 IEEE 39th Annual Computer Software and Applications Conference, COMPSAC 2015",

}

Benghabrit, W, Grall, H, Royer, JC & Sellami, M 2015, Checking Accountability with a Prover. in G Huang, J Yang, SI Ahamed, P-A Hsiung, CK Chang, W Chu & I Crnkovic (eds), Proceedings - 2015 IEEE 39th Annual Computer Software and Applications Conference, COMPSAC 2015., 7273604, Proceedings - International Computer Software and Applications Conference, vol. 2, IEEE Computer Society, pp. 83-88, 39th IEEE Annual Computer Software and Applications Conference, COMPSAC 2015, Taichung, Taiwan, Province of China, 1/07/15. https://doi.org/10.1109/COMPSAC.2015.8

Checking Accountability with a Prover. / Benghabrit, Walid; Grall, Herve; Royer, Jean Claude et al.
Proceedings - 2015 IEEE 39th Annual Computer Software and Applications Conference, COMPSAC 2015. ed. / Gang Huang; Jingwei Yang; Sheikh Iqbal Ahamed; Pao-Ann Hsiung; Carl K. Chang; William Chu; Ivica Crnkovic. IEEE Computer Society, 2015. p. 83-88 7273604 (Proceedings - International Computer Software and Applications Conference; Vol. 2).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Checking Accountability with a Prover

AU - Benghabrit, Walid

AU - Grall, Herve

AU - Royer, Jean Claude

AU - Sellami, Mohamed

PY - 2015/9/21

Y1 - 2015/9/21

N2 - Today on-line services are the cornerstone of on-line applications such as e-commerce, e-government and e-health applications. However, they raise several challenges about data privacy. Accountability, which is the property of an entity of being responsible for its acts, meets some of these challenges and hence increases user's trustworthiness in on-line applications. In this work, we propose an approach to assist the design of accountable applications. In particular, we consider an application's abstract component design and we introduce a logical approach allowing various static verifications. This approach offers effective means to early check the design and the behavior of an application and its offered/required services. We motivate our work with a realistic use case coming from the A4Cloud project and validate our proposal with experiments using a theorem prover.

AB - Today on-line services are the cornerstone of on-line applications such as e-commerce, e-government and e-health applications. However, they raise several challenges about data privacy. Accountability, which is the property of an entity of being responsible for its acts, meets some of these challenges and hence increases user's trustworthiness in on-line applications. In this work, we propose an approach to assist the design of accountable applications. In particular, we consider an application's abstract component design and we introduce a logical approach allowing various static verifications. This approach offers effective means to early check the design and the behavior of an application and its offered/required services. We motivate our work with a realistic use case coming from the A4Cloud project and validate our proposal with experiments using a theorem prover.

KW - Accountability language

KW - Component diagram

KW - First-order temporal logic

KW - Prover

KW - Software design

KW - Verification

U2 - 10.1109/COMPSAC.2015.8

DO - 10.1109/COMPSAC.2015.8

M3 - Conference contribution

AN - SCOPUS:84962193500

T3 - Proceedings - International Computer Software and Applications Conference

SP - 83

EP - 88

BT - Proceedings - 2015 IEEE 39th Annual Computer Software and Applications Conference, COMPSAC 2015

A2 - Huang, Gang

A2 - Yang, Jingwei

A2 - Ahamed, Sheikh Iqbal

A2 - Hsiung, Pao-Ann

A2 - Chang, Carl K.

A2 - Chu, William

A2 - Crnkovic, Ivica

PB - IEEE Computer Society

T2 - 39th IEEE Annual Computer Software and Applications Conference, COMPSAC 2015

Y2 - 1 July 2015 through 5 July 2015

ER -

Benghabrit W, Grall H, Royer JC, Sellami M. Checking Accountability with a Prover. In Huang G, Yang J, Ahamed SI, Hsiung PA, Chang CK, Chu W, Crnkovic I, editors, Proceedings - 2015 IEEE 39th Annual Computer Software and Applications Conference, COMPSAC 2015. IEEE Computer Society. 2015. p. 83-88. 7273604. (Proceedings - International Computer Software and Applications Conference). doi: 10.1109/COMPSAC.2015.8

Checking Accountability with a Prover

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this