A proof-based approach to verifying reachability properties

Amel Mammar; Marc Frappier; Fama Diagne

doi:10.1145/1982185.1982531

A proof-based approach to verifying reachability properties

Amel Mammar
, Marc Frappier
, Fama Diagne

Université de Sherbrooke
CNRS UMR 5157 SAMOVAR

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

Abstract

This paper presents a formal approach to proving temporal reachability properties, expressed in CTL, on B systems. We are particularly interested in demonstrating that a system can reach a given state by executing a sequence of actions (or operation calls) called a path. Starting with a path, the proposed approach consists in calculating the proof obligations to discharge in order to prove that the path allows the system to evolve in order to verify the desired property. Since these proof obligations are expressed as first logic formulas without any temporal operator, they can be discharged using the prover of AtelierB. Our proposal is illustrated through a case study.

Original language	English
Title of host publication	26th Annual ACM Symposium on Applied Computing, SAC 2011
Pages	1651-1657
Number of pages	7
DOIs	https://doi.org/10.1145/1982185.1982531
Publication status	Published - 23 Jun 2011
Event	26th Annual ACM Symposium on Applied Computing, SAC 2011 - TaiChung, Taiwan, Province of China Duration: 21 Mar 2011 → 24 Mar 2011

Publication series

Name	Proceedings of the ACM Symposium on Applied Computing

Conference

Conference	26th Annual ACM Symposium on Applied Computing, SAC 2011
Country/Territory	Taiwan, Province of China
City	TaiChung
Period	21/03/11 → 24/03/11

Keywords

B language
CTL formulas
proof obligations
reachability properties

Access to Document

10.1145/1982185.1982531

Cite this

@inproceedings{2ad52500711f49c0936e7cd2d8f86a37,

title = "A proof-based approach to verifying reachability properties",

abstract = "This paper presents a formal approach to proving temporal reachability properties, expressed in CTL, on B systems. We are particularly interested in demonstrating that a system can reach a given state by executing a sequence of actions (or operation calls) called a path. Starting with a path, the proposed approach consists in calculating the proof obligations to discharge in order to prove that the path allows the system to evolve in order to verify the desired property. Since these proof obligations are expressed as first logic formulas without any temporal operator, they can be discharged using the prover of AtelierB. Our proposal is illustrated through a case study.",

keywords = "B language, CTL formulas, proof obligations, reachability properties",

author = "Amel Mammar and Marc Frappier and Fama Diagne",

year = "2011",

month = jun,

day = "23",

doi = "10.1145/1982185.1982531",

language = "English",

isbn = "9781450301138",

series = "Proceedings of the ACM Symposium on Applied Computing",

pages = "1651--1657",

booktitle = "26th Annual ACM Symposium on Applied Computing, SAC 2011",

note = "26th Annual ACM Symposium on Applied Computing, SAC 2011 ; Conference date: 21-03-2011 Through 24-03-2011",

}

Mammar, A, Frappier, M & Diagne, F 2011, A proof-based approach to verifying reachability properties. in 26th Annual ACM Symposium on Applied Computing, SAC 2011. Proceedings of the ACM Symposium on Applied Computing, pp. 1651-1657, 26th Annual ACM Symposium on Applied Computing, SAC 2011, TaiChung, Taiwan, Province of China, 21/03/11. https://doi.org/10.1145/1982185.1982531

TY - GEN

T1 - A proof-based approach to verifying reachability properties

AU - Mammar, Amel

AU - Frappier, Marc

AU - Diagne, Fama

PY - 2011/6/23

Y1 - 2011/6/23

N2 - This paper presents a formal approach to proving temporal reachability properties, expressed in CTL, on B systems. We are particularly interested in demonstrating that a system can reach a given state by executing a sequence of actions (or operation calls) called a path. Starting with a path, the proposed approach consists in calculating the proof obligations to discharge in order to prove that the path allows the system to evolve in order to verify the desired property. Since these proof obligations are expressed as first logic formulas without any temporal operator, they can be discharged using the prover of AtelierB. Our proposal is illustrated through a case study.

AB - This paper presents a formal approach to proving temporal reachability properties, expressed in CTL, on B systems. We are particularly interested in demonstrating that a system can reach a given state by executing a sequence of actions (or operation calls) called a path. Starting with a path, the proposed approach consists in calculating the proof obligations to discharge in order to prove that the path allows the system to evolve in order to verify the desired property. Since these proof obligations are expressed as first logic formulas without any temporal operator, they can be discharged using the prover of AtelierB. Our proposal is illustrated through a case study.

KW - B language

KW - CTL formulas

KW - proof obligations

KW - reachability properties

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

U2 - 10.1145/1982185.1982531

DO - 10.1145/1982185.1982531

M3 - Conference contribution

AN - SCOPUS:79959313463

SN - 9781450301138

T3 - Proceedings of the ACM Symposium on Applied Computing

SP - 1651

EP - 1657

BT - 26th Annual ACM Symposium on Applied Computing, SAC 2011

T2 - 26th Annual ACM Symposium on Applied Computing, SAC 2011

Y2 - 21 March 2011 through 24 March 2011

ER -

A proof-based approach to verifying reachability properties

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this