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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507–534, may 1995.
J.R. Abrial. The B-Book. Cambridge University Press, 1996.
D.J. Andrews, H. Bruun, B.S. Hansen, P.G. Larsen, N. Plat, and all. Information Technology-Programming Languages, their environments and system software interfaces-Vienna Development Method-Specification Language Part 1: Base language. ISO, 1995.
P. Behm, P. Benoit, A. Faivre, and J.-M. Meynadier. Météor: A Successful Application of B in a Large Project. LNCS, FM’99-Formal Methods, 1:348–387, september 1999.
Grady Booch. Object-Oriented Analysis and Design. Addison-Wesley, 1994.
R. Elmstrom, P. G. Larsen, and P. B. Lassen. The IFAD VDM-SL toolbox: a practical approach to formal specifications. ACM SIGPLAN Notices, 29(9):77–80, 1994.
RAISE Language Group. The RAISE Specification Language. Prentice Hall-BCS Practioner series, 1992.
The VDM-SL Tool Group. Users Manual for the IFAD VDM-SL Toolbox. IFAD, Forskerparken 10, 5230 Odense M, Denmark, February 1994. IFAD-VDM-4.
C. B. Jones. Systematic Software Development Using VDM (Second Edition). Prentice-Hall, London, 1990.
L. Mussat and J.R. Abrial. Introducing Dynamic Constraints in B. In D. Bert, editor, Proceedings of the Second International B Conference, volume 1393 of Lecture Notes in Computer Science. Springer-Verlag, 1998.
M.-L. Potet and Y. Rouzaud. Composition and Refinement in the B-method. In D. Bert, editor, Proceedings of the Second International B Conference, volume 1393 of Lecture Notes in Computer Science. Springer-Verlag, 1998.
C.A. Middelburg. Logic and Specification: Extending VDM-SL for advanced formal specification. Chapman and Hall, 1993.
D. Parnas. On the criteria to be used in decomposing systems into modules. Communications of the ACM, 15(12):1053–1058, december 1972.
J.M. Spivey. The Z notation-A Reference Manual (Second Edition). Prentice Hall, 1992.
M. Srinivas and L.M. Patnaik. Genetic algorithms: a survey. IEEE Computer, pages 17–26, june 1994.
Y.V. Srinivas and R. Jüllig. Specware(TM): Formal support for composing software. Technical Report KES.U.94.5, Kestrel Institute, december 1994.
Y.V. Srinivas and R. Jüllig. Specware Language Manual. Kestrel Institute, November 1995.
Y. Ledru, C. Oriat, and M-L. Potet. Le raffinement vu comme primitive de spécification-une comparaison de VDM, B et Specware. Technical report, AFADL Approches Formelles dans l’Assistance au Développement de Logiciels, LISI/ENSMA, 86960 FUTUROSCOPE, 1998.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bontron, P., Potet, ML. (2000). Automatic Construction of Validated B Components from Structured Developments. In: ZB 2000: Formal Specification and Development in Z and B. ZB 2000. Lecture Notes in Computer Science, vol 1878. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44525-0_9
Download citation
DOI: https://doi.org/10.1007/3-540-44525-0_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67944-8
Online ISBN: 978-3-540-44525-8
eBook Packages: Springer Book Archive