Developing BON as an Industrial-Strength Formal Method

Richard F. Paige; Jonathan S. Ostroff

doi:10.1007/3-540-48119-2_46

Developing BON as an Industrial-Strength Formal Method

Richard F. Paige, Jonathan S. Ostroff

Computer Science

Research output: Contribution to conference › Paper › peer-review

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.

Original language	Undefined/Unknown
Pages	834-853
DOIs	https://doi.org/10.1007/3-540-48119-2_46
Publication status	Published - 1999

Access to Document

10.1007/3-540-48119-2_46

http://link.springer.de/link/service/series/0558/bibs/1708/17080834.htm

Cite this

@conference{cf2a2140f5b543e0b37e39699703ea13,

title = "Developing BON as an Industrial-Strength Formal Method",

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. ",

author = "Paige, {Richard F.} and Ostroff, {Jonathan S.}",

year = "1999",

doi = "10.1007/3-540-48119-2_46",

language = "Undefined/Unknown",

pages = "834--853",

}

TY - CONF

T1 - Developing BON as an Industrial-Strength Formal Method

AU - Paige, Richard F.

AU - Ostroff, Jonathan S.

PY - 1999

Y1 - 1999

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

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

U2 - 10.1007/3-540-48119-2_46

DO - 10.1007/3-540-48119-2_46

M3 - Paper

SP - 834

EP - 853

ER -