Paper Info
Title
Interpreting invariant composition in the b method using the spec# ownership relation: a way to explain and relax b restrictions
Abstract
In the B method, the invariant of a component cannot be violated outside its own operations. This approach has a great advantage: the users of a component can assume its invariant without having to prove it. But, B users must deal with important architecture restrictions that ensure the soundness of reasonings involving invariants. Moreover, understanding how these restrictions ensure soundness is not trivial. This paper studies a meta-model of invariant composition, inspired from the Spec# approach. Basically, in this model, invariant violations are monitored using ghost variables. The consistency of assumptions about invariants is controlled by very simple proof obligations. Hence, this model provides a simple framework to understand B composition rules and to study some conservative extensions of B authorizing more architectures and providing more control on components initialization.
Year
DOI
Venue
2007
10.1007/11955757_4
B
Keywords
Field
DocType
b method,simple proof obligation,invariant composition,ghost variable,b restriction,conservative extension,ownership relation,b user,b composition rule,components initialization,invariant violation,simple framework,meta model
Discrete mathematics,Algebra,Computer science,Algorithm,Formal specification,B-Method,Invariant (mathematics),Initialization,Soundness,Spec#,Metamodeling,Software development
Conference
Volume
ISSN
ISBN
4355
0302-9743
3-540-68760-2
Citations 
PageRank 
References 
3
0.39
16
Authors
2
Name
Order
Citations
PageRank
Sylvain Boulmé1505.69
Marie-Laure Potet219021.34