Proof-based verification approaches for dynamic properties: application to the information system domain

Amel Mammar; Marc Frappier

doi:10.1007/s00165-014-0323-x

Proof-based verification approaches for dynamic properties: application to the information system domain

Amel Mammar
, Marc Frappier

Université de Sherbrooke

Research output: Contribution to journal › Article › peer-review

Abstract

This paper proposes a formal approach for generating necessary and sufficient proof obligations to demonstrate a set of dynamic properties using the B method. In particular, we consider reachability, non-interference and absence properties. Also, we show that these properties permit a wide range of property patterns introduced by Dwyer to be expressed. An overview of a tool supporting these approaches is also provided.

Original language	English
Pages (from-to)	335-374
Number of pages	40
Journal	Formal Aspects of Computing
Volume	27
Issue number	2
DOIs	https://doi.org/10.1007/s00165-014-0323-x
Publication status	Published - 1 Mar 2015

Keywords

B formal method
Dynamic properties
Proof
Property patterns

Access to Document

10.1007/s00165-014-0323-x

Cite this

@article{b152cbe3b9474bc08ef43f410ff23805,

title = "Proof-based verification approaches for dynamic properties: application to the information system domain",

abstract = "This paper proposes a formal approach for generating necessary and sufficient proof obligations to demonstrate a set of dynamic properties using the B method. In particular, we consider reachability, non-interference and absence properties. Also, we show that these properties permit a wide range of property patterns introduced by Dwyer to be expressed. An overview of a tool supporting these approaches is also provided.",

keywords = "B formal method, Dynamic properties, Proof, Property patterns",

author = "Amel Mammar and Marc Frappier",

note = "Publisher Copyright: {\textcopyright} 2014, British Computer Society.",

year = "2015",

month = mar,

day = "1",

doi = "10.1007/s00165-014-0323-x",

language = "English",

volume = "27",

pages = "335--374",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

number = "2",

}

TY - JOUR

T1 - Proof-based verification approaches for dynamic properties

T2 - application to the information system domain

AU - Mammar, Amel

AU - Frappier, Marc

PY - 2015/3/1

Y1 - 2015/3/1

N2 - This paper proposes a formal approach for generating necessary and sufficient proof obligations to demonstrate a set of dynamic properties using the B method. In particular, we consider reachability, non-interference and absence properties. Also, we show that these properties permit a wide range of property patterns introduced by Dwyer to be expressed. An overview of a tool supporting these approaches is also provided.

AB - This paper proposes a formal approach for generating necessary and sufficient proof obligations to demonstrate a set of dynamic properties using the B method. In particular, we consider reachability, non-interference and absence properties. Also, we show that these properties permit a wide range of property patterns introduced by Dwyer to be expressed. An overview of a tool supporting these approaches is also provided.

KW - B formal method

KW - Dynamic properties

KW - Proof

KW - Property patterns

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

U2 - 10.1007/s00165-014-0323-x

DO - 10.1007/s00165-014-0323-x

M3 - Article

AN - SCOPUS:84925485251

SN - 0934-5043

VL - 27

SP - 335

EP - 374

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 2

ER -

Proof-based verification approaches for dynamic properties: application to the information system domain

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this