Proving the Absence Property Pattern Using the B Method

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 form...

Full description

Saved in:
Bibliographic Details
Main Authors: Mammar, A., Frappier, M., Chane-Yack-Fa, R.
Format: Conference Proceeding
Language:English
Subjects:
Absence patterns
B Method
Conferences
Information systems
Marketing and sales
Proposals
Safety
Temporal properties
Unified modeling language
Verification
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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(P 2 , From P 1 Until P 3 ) that express that some states, represented by predicate P 2 , should not be reached starting from a state that satisfies P 1 until a state satisfies P 3 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.
ISSN:1530-2059
2640-7507
DOI:10.1109/HASE.2012.26