Abstract
The emerging Unified Modelling Language has been touted as merging the best features of existing modelling languages, and has been adopted by leading companies and vendors as a universal software modelling language. Some researchers are also looking to UML as a basis for formal methods development. A less known approach is BON (the Business Object Notation), which is based on the principles of seamlessness, reversibility and design by contract, making it an ideal basis for industrial-strength formal methods development of object-oriented software. In this paper, we argue that BON is much more suited for the application of formal methods than UML. We describe the properties that an industrial-strength formal method must have, show how algorithm refinement can be done in BON (as an example of using BON for formal development), and contrast BON with other approaches, including UML, Z, B and VDM.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J.-R. Abrial. The B-Book, Cambridge, 1996.
L. Baresi and M. Pezze. Toward Formalizing Structured Analysis, ACM Trans. Soft. Eng. Method. 7(1), January 1998.
J. Bicarregui, B. Matthews, and B. Ritchie. Investigating the integration of two formal methods. In Proc. FMICS’ 98, CWI, 1998.
A. Evans, R. France, K. Lano, and B. Rumpe. The UML as a Formal Modeling Notation. Computer Standards and Interfaces 19(7), 1998.
M. Fowler. UML Distilled, Addison-Wesley, 1997.
D. Gries and F. Schneider. A Logical Approach to Discrete Math, Springer, 1993.
A. Hall. Seven Myths of Formal Methods. IEEE Software, September 1990.
L. Hatton. Does OO Sync with How We Think? IEEE Software, May/June 1998.
E.C.R. Hehner. A Practical Theory of Programming, Springer-Verlag, 1993.
B. Jacobs et al. Reasoning about Java Classes (Preliminary Report). In Proc. OOPSLA’98, ACM Press, Oct. 1998.
C.B. Jones. Systematic Software Development using VDM, Prentice-Hall, 1990.
L. Lo. Modular Design for Reactive Systems,MSc Thesis, Department of Computer Science, York University, 1998.
B. Matthews, B. Ritchie, and J. Bicarregui. Synthesizing structure from flat specifications. In Proc. B’98, LNCS 1393, Springer-Verlag, 1998.
B. Meyer. Object-Oriented Software Construction, Prentice-Hal, 1997.
J.S. Ostroff. Temporal Logic for Real-Time Systems, Wiley, 1989
J.S. Ostroff and R.F. Paige. Formal Methods in the Classroom: The Logic of Real-Time Software Design. In Proc. Real-Time Software Engineering Education Workshop’98, IEEE Press, 1999.
R.F. Paige. A Meta-Method for Formal Method Integration. In Proc. FME’97, LNCS 1313, Springer, 1997.
R.F. Paige. Heterogeneous Notations for Pure Formal Method Integration. Formal Aspects of Computing 10(3):233–242, June 1999.
R.F. Paige and J.S. Ostroff. A Comparison of BON and UML. Technical Report CS-1999-03, York University, May 1999.
J.M. Spivey. The Z Notation: A Reference Manual, Prentice-Hall, 1989.
K. Walden and J.-M. Nerson. Seamless Object-Oriented Software Development, Prentice-Hall, 1995.
D. Weber-Wulff. Selling Formal Methods to Industry. In Proc. FME’ 93, LNCS 670, Springer-Verlag, 1993.
J. Wordsworth. Software Development with Z, Addison-Wesley, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Paige, R.F., Ostroff, J.S. (1999). Developing BON as an Industrial-Strength Formal Method. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48119-2_46
Download citation
DOI: https://doi.org/10.1007/3-540-48119-2_46
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66587-8
Online ISBN: 978-3-540-48119-5
eBook Packages: Springer Book Archive