Skip Navigation
York U: Redefine the PossibleHOME | Current Students | Faculty & Staff | Research | International
Search »FacultiesLibrariesCampus MapsYork U OrganizationDirectorySite Index
Future Students, Alumni & Visitors
2002 Technical Reports

Checking the Consistency of Views using PVS

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

Technical Report CS-2002-01

York University

February 18, 2002

Abstract

A method, based on BON for building reliable object-oriented software systems was proposed in [14]. It combined use of modelling and Extreme Programming (XP) practices, emphasizing the use of a limited set of views of a software system, with consistency rules and automatic generation tools defined between the views. This paper builds upon this framework and formally specifies the consistency constraints between the two BON views: the static view provided by class diagrams, and the dynamic view provided by collaboration diagrams. The constraints are specified as an extension of the BON metamodel from [12], and are implemented in PVS. They ensure that the sequence of messages appearing in the dynamic view are permitted, given the contracts appearing in the static view. A sketch of how the constraints might be implemented in a BON CASE tool is also provided.

(A revised version of this paper was published in Proc. Fourth Workshop on Rigorous Object-Oriented Methods (ROOM4), London, UK, Springer, March 2002.)

Download paper in PDF format.



The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.