Verifying the precedence property pattern using the B method

Amel Mammar; Marc Frappier

doi:10.1109/HASE.2014.40

Verifying the precedence property pattern using the B method

Amel Mammar
, Marc Frappier

Université de Sherbrooke

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

Abstract

This paper presents an approach to proving a temporal property pattern of the form Prec(P₁, P₂) that expresses that if a state, presented by predicate P₂, is reached then there should exist a state, in the past, that verifies P₁. Such a property pattern is very useful in the specification of various systems such as Information Systems (IS) and security policies. To this aim, we define sufficient and necessary proof obligations that allow to establish such a property.

Original language	English
Pages	229-233
Number of pages	5
DOIs	https://doi.org/10.1109/HASE.2014.40
Publication status	Published - 1 Jan 2014
Event	2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014 - Miami, FL, United States Duration: 9 Jan 2014 → 11 Jan 2014

Conference

Conference	2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014
Country/Territory	United States
City	Miami, FL
Period	9/01/14 → 11/01/14

Keywords

B Method
Precedence properties
Proofs
Temporal properties
Verification

Access to Document

10.1109/HASE.2014.40

Cite this

@conference{cdc1aee47a664ab4b834b1239b96e45e,

title = "Verifying the precedence property pattern using the B method",

abstract = "This paper presents an approach to proving a temporal property pattern of the form Prec(P1, P2) that expresses that if a state, presented by predicate P2, is reached then there should exist a state, in the past, that verifies P1. Such a property pattern is very useful in the specification of various systems such as Information Systems (IS) and security policies. To this aim, we define sufficient and necessary proof obligations that allow to establish such a property.",

keywords = "B Method, Precedence properties, Proofs, Temporal properties, Verification",

author = "Amel Mammar and Marc Frappier",

year = "2014",

month = jan,

day = "1",

doi = "10.1109/HASE.2014.40",

language = "English",

pages = "229--233",

note = "2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014 ; Conference date: 09-01-2014 Through 11-01-2014",

}

TY - CONF

T1 - Verifying the precedence property pattern using the B method

AU - Mammar, Amel

AU - Frappier, Marc

PY - 2014/1/1

Y1 - 2014/1/1

N2 - This paper presents an approach to proving a temporal property pattern of the form Prec(P1, P2) that expresses that if a state, presented by predicate P2, is reached then there should exist a state, in the past, that verifies P1. Such a property pattern is very useful in the specification of various systems such as Information Systems (IS) and security policies. To this aim, we define sufficient and necessary proof obligations that allow to establish such a property.

AB - This paper presents an approach to proving a temporal property pattern of the form Prec(P1, P2) that expresses that if a state, presented by predicate P2, is reached then there should exist a state, in the past, that verifies P1. Such a property pattern is very useful in the specification of various systems such as Information Systems (IS) and security policies. To this aim, we define sufficient and necessary proof obligations that allow to establish such a property.

KW - B Method

KW - Precedence properties

KW - Proofs

KW - Temporal properties

KW - Verification

U2 - 10.1109/HASE.2014.40

DO - 10.1109/HASE.2014.40

M3 - Paper

AN - SCOPUS:84898639922

SP - 229

EP - 233

T2 - 2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014

Y2 - 9 January 2014 through 11 January 2014

ER -

Verifying the precedence property pattern using the B method

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this