Proving the absence property pattern using the B method

Amel Mammar; Marc Frappier; Raphael Chane-Yack-Fa

doi:10.1109/HASE.2012.26

Proving the absence property pattern using the B method

Amel Mammar
, Marc Frappier
, Raphael Chane-Yack-Fa

Université de Sherbrooke

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

Abstract

Dynamic properties are very useful in the specification of Information Systems (IS) and security policies. They allow the user to express properties that involve several states of a system. Indeed, invariance properties do not permit to cover such kind of properties. In this paper, we suggest a formal approach, based on the use of the B method, to verifying absence properties of the form Abs(P₂, From P₁ Until P₃) that express that some states, represented by predicate P₂, should not be reached starting from a state that satisfies P₁ until a state satisfies P₃ is reached. Our proposal consists in defining two proof obligations based on weakest preconditions that are sufficient and necessary to prove that a system verifies such a property.

Original language	English
Title of host publication	Proceedings - IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012
Pages	167-170
Number of pages	4
DOIs	https://doi.org/10.1109/HASE.2012.26
Publication status	Published - 1 Dec 2012
Event	IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012 - Omaha, NE, United States Duration: 25 Oct 2012 → 27 Oct 2012

Publication series

Name	Proceedings of IEEE International Symposium on High Assurance Systems Engineering
ISSN (Print)	1530-2059

Conference

Conference	IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012
Country/Territory	United States
City	Omaha, NE
Period	25/10/12 → 27/10/12

Keywords

Absence patterns
B Method
Temporal properties
Verification

Access to Document

10.1109/HASE.2012.26

Cite this

@inproceedings{c5cd0ef3984842169b5f9cbdc5c45c36,

title = "Proving the absence property pattern using the B method",

abstract = "Dynamic properties are very useful in the specification of Information Systems (IS) and security policies. They allow the user to express properties that involve several states of a system. Indeed, invariance properties do not permit to cover such kind of properties. In this paper, we suggest a formal approach, based on the use of the B method, to verifying absence properties of the form Abs(P2, From P1 Until P3) that express that some states, represented by predicate P2, should not be reached starting from a state that satisfies P1 until a state satisfies P3 is reached. Our proposal consists in defining two proof obligations based on weakest preconditions that are sufficient and necessary to prove that a system verifies such a property.",

keywords = "Absence patterns, B Method, Temporal properties, Verification",

author = "Amel Mammar and Marc Frappier and Raphael Chane-Yack-Fa",

year = "2012",

month = dec,

day = "1",

doi = "10.1109/HASE.2012.26",

language = "English",

isbn = "9780769549125",

series = "Proceedings of IEEE International Symposium on High Assurance Systems Engineering",

pages = "167--170",

booktitle = "Proceedings - IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012",

note = "IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012 ; Conference date: 25-10-2012 Through 27-10-2012",

}

Mammar, A, Frappier, M & Chane-Yack-Fa, R 2012, Proving the absence property pattern using the B method. in Proceedings - IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012., 6375612, Proceedings of IEEE International Symposium on High Assurance Systems Engineering, pp. 167-170, IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012, Omaha, NE, United States, 25/10/12. https://doi.org/10.1109/HASE.2012.26

Proving the absence property pattern using the B method. / Mammar, Amel; Frappier, Marc; Chane-Yack-Fa, Raphael.
Proceedings - IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012. 2012. p. 167-170 6375612 (Proceedings of IEEE International Symposium on High Assurance Systems Engineering).

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

TY - GEN

T1 - Proving the absence property pattern using the B method

AU - Mammar, Amel

AU - Frappier, Marc

AU - Chane-Yack-Fa, Raphael

PY - 2012/12/1

Y1 - 2012/12/1

N2 - Dynamic properties are very useful in the specification of Information Systems (IS) and security policies. They allow the user to express properties that involve several states of a system. Indeed, invariance properties do not permit to cover such kind of properties. In this paper, we suggest a formal approach, based on the use of the B method, to verifying absence properties of the form Abs(P2, From P1 Until P3) that express that some states, represented by predicate P2, should not be reached starting from a state that satisfies P1 until a state satisfies P3 is reached. Our proposal consists in defining two proof obligations based on weakest preconditions that are sufficient and necessary to prove that a system verifies such a property.

AB - Dynamic properties are very useful in the specification of Information Systems (IS) and security policies. They allow the user to express properties that involve several states of a system. Indeed, invariance properties do not permit to cover such kind of properties. In this paper, we suggest a formal approach, based on the use of the B method, to verifying absence properties of the form Abs(P2, From P1 Until P3) that express that some states, represented by predicate P2, should not be reached starting from a state that satisfies P1 until a state satisfies P3 is reached. Our proposal consists in defining two proof obligations based on weakest preconditions that are sufficient and necessary to prove that a system verifies such a property.

KW - Absence patterns

KW - B Method

KW - Temporal properties

KW - Verification

UR - https://www.scopus.com/pages/publications/84871944246

U2 - 10.1109/HASE.2012.26

DO - 10.1109/HASE.2012.26

M3 - Conference contribution

AN - SCOPUS:84871944246

SN - 9780769549125

T3 - Proceedings of IEEE International Symposium on High Assurance Systems Engineering

SP - 167

EP - 170

BT - Proceedings - IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012

T2 - IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012

Y2 - 25 October 2012 through 27 October 2012

ER -

Proving the absence property pattern using the B method

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this