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

Résultats de recherche: Contribution à une conférence › Papier › Revue par des pairs

Résumé

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.

langue originale	Anglais
Pages	229-233
Nombre de pages	5
Les DOIs	https://doi.org/10.1109/HASE.2014.40
état	Publié - 1 janv. 2014
Evénement	2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014 - Miami, FL, États-Unis Durée: 9 janv. 2014 → 11 janv. 2014

Une conférence

Une conférence	2014 IEEE 15th International Symposium on High-Assurance Systems Engineering, HASE 2014
Pays/Territoire	États-Unis
La ville	Miami, FL
période	9/01/14 → 11/01/14

Accès au document

10.1109/HASE.2014.40

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

@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

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

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

Résumé

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation