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 -