Paper Info
Title
Automatic Construction of Validated B Components from Structured Developments
Abstract
Decomposition and refinement provide a way to master the complexity of system specification and development. Decomposition allows us to describe a complex system in term of simpler and more understandable components and in terms of the interactions between these components. Refinement/Abstraction allows us to use more general specifications, which should also be more understandable, and which can be gradually made more precise. Combining decomposition and refinement offers a very powerful tool to build specifications. This process results in a structured object which describes both the final specification and its elaboration in term of interaction and refinement. Nevertheless the result remains intrinsically a complex object. The next step consists in developing tools to represent, to manipulate and to reason about such structured objects. The aim of this paper is to propose such a tool in the framework of the B method. By exploiting the B theory, and as far as possible without changing the method, we propose three algorithms to extract validated B components, using properties underlying the structure of developments. These new components can be exploited to extend a structured development, for instance to validate new properties.
Year
DOI
Venue
2000
10.1007/3-540-44525-0_9
ZB
Keywords
Field
DocType
b method,validated b components,complex system,b component,structured development,automatic construction,combining decomposition,final specification,structured object,b theory,complex object,general specification,structured developments
Programming language,Abstraction,Computer science,B-Method,Artificial intelligence,Proof obligation,System requirements specification,Elaboration,Abstract machine,Distributed computing
Conference
ISBN
Citations 
PageRank 
3-540-67944-8
3
0.44
References 
Authors
9
2
Name
Order
Citations
PageRank
Pierre Bontron1342.49
Marie-Laure Potet219021.34