Theorem Proving Support for View Consistency Checking

Richard F. Paige; Jonathan S. Ostroff; Phillip J Brooke

doi:10.3166/objet.9.4.115-134

Theorem Proving Support for View Consistency Checking

Richard F. Paige
, Jonathan S. Ostroff
, Phillip J Brooke

Research output: Contribution to journal › Article › peer-review

Abstract

A formal, mechanically checked specification of the consistency constraints between two views of object-oriented systems are presented. The views, described in the BON modelling language, capture the static architecture of systems via contract-annotated class diagrams, and the dynamic view provided by collaboration diagrams. The constraints are specified as an extension of the BON metamodel, and are implemented in PVS. They ensure that the sequence of messages appearing in the dynamic view is legal, given the pre- and postconditions of methods appearing in the static view. An example of how the PVS theorem prover might be used to verify view consistency is described.

Original language	English
Pages (from-to)	115-134
Journal	L'objet
Volume	9
Issue number	4
DOIs	https://doi.org/10.3166/objet.9.4.115-134
Publication status	Published - 30 Dec 2003

Access to Document

10.3166/objet.9.4.115-134

http://objet.revuesonline.com/article.jsp?articleId=3633

Cite this

@article{68b4b73aa7a14c0d82fa53126f8caf6e,

title = "Theorem Proving Support for View Consistency Checking",

abstract = "A formal, mechanically checked specification of the consistency constraints between two views of object-oriented systems are presented. The views, described in the BON modelling language, capture the static architecture of systems via contract-annotated class diagrams, and the dynamic view provided by collaboration diagrams. The constraints are specified as an extension of the BON metamodel, and are implemented in PVS. They ensure that the sequence of messages appearing in the dynamic view is legal, given the pre- and postconditions of methods appearing in the static view. An example of how the PVS theorem prover might be used to verify view consistency is described.",

author = "Paige, \{Richard F.\} and Ostroff, \{Jonathan S.\} and Brooke, \{Phillip J\}",

year = "2003",

month = dec,

day = "30",

doi = "10.3166/objet.9.4.115-134",

language = "English",

volume = "9",

pages = "115--134",

journal = "L'objet",

issn = "1262-1137",

publisher = "Lavoisier",

number = "4",

}

TY - JOUR

T1 - Theorem Proving Support for View Consistency Checking

AU - Paige, Richard F.

AU - Ostroff, Jonathan S.

AU - Brooke, Phillip J

PY - 2003/12/30

Y1 - 2003/12/30

N2 - A formal, mechanically checked specification of the consistency constraints between two views of object-oriented systems are presented. The views, described in the BON modelling language, capture the static architecture of systems via contract-annotated class diagrams, and the dynamic view provided by collaboration diagrams. The constraints are specified as an extension of the BON metamodel, and are implemented in PVS. They ensure that the sequence of messages appearing in the dynamic view is legal, given the pre- and postconditions of methods appearing in the static view. An example of how the PVS theorem prover might be used to verify view consistency is described.

AB - A formal, mechanically checked specification of the consistency constraints between two views of object-oriented systems are presented. The views, described in the BON modelling language, capture the static architecture of systems via contract-annotated class diagrams, and the dynamic view provided by collaboration diagrams. The constraints are specified as an extension of the BON metamodel, and are implemented in PVS. They ensure that the sequence of messages appearing in the dynamic view is legal, given the pre- and postconditions of methods appearing in the static view. An example of how the PVS theorem prover might be used to verify view consistency is described.

U2 - 10.3166/objet.9.4.115-134

DO - 10.3166/objet.9.4.115-134

M3 - Article

SN - 1262-1137

VL - 9

SP - 115

EP - 134

JO - L'objet

JF - L'objet

IS - 4

ER -

Theorem Proving Support for View Consistency Checking

Abstract

Access to Document

Fingerprint

Cite this