TY - GEN
T1 - Proving the absence property pattern using the B method
AU - Mammar, Amel
AU - Frappier, Marc
AU - Chane-Yack-Fa, Raphael
PY - 2012/12/1
Y1 - 2012/12/1
N2 - Dynamic properties are very useful in the specification of Information Systems (IS) and security policies. They allow the user to express properties that involve several states of a system. Indeed, invariance properties do not permit to cover such kind of properties. In this paper, we suggest a formal approach, based on the use of the B method, to verifying absence properties of the form Abs(P2, From P1 Until P3) that express that some states, represented by predicate P2, should not be reached starting from a state that satisfies P1 until a state satisfies P3 is reached. Our proposal consists in defining two proof obligations based on weakest preconditions that are sufficient and necessary to prove that a system verifies such a property.
AB - Dynamic properties are very useful in the specification of Information Systems (IS) and security policies. They allow the user to express properties that involve several states of a system. Indeed, invariance properties do not permit to cover such kind of properties. In this paper, we suggest a formal approach, based on the use of the B method, to verifying absence properties of the form Abs(P2, From P1 Until P3) that express that some states, represented by predicate P2, should not be reached starting from a state that satisfies P1 until a state satisfies P3 is reached. Our proposal consists in defining two proof obligations based on weakest preconditions that are sufficient and necessary to prove that a system verifies such a property.
KW - Absence patterns
KW - B Method
KW - Temporal properties
KW - Verification
U2 - 10.1109/HASE.2012.26
DO - 10.1109/HASE.2012.26
M3 - Conference contribution
AN - SCOPUS:84871944246
SN - 9780769549125
T3 - Proceedings of IEEE International Symposium on High Assurance Systems Engineering
SP - 167
EP - 170
BT - Proceedings - IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012
T2 - IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012
Y2 - 25 October 2012 through 27 October 2012
ER -