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 -