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

Precise and Formal Metamodeling with the Business Object Notation and PVS

Richard F. Paige and Jonathan S. Ostroff

Technical Report CS-2000-03

York University

August 9, 2000


A modeling language consists of both a notation and a metamodel, the latter of which captures the syntactic well-formedness constraints that all valid models must obey. We present two versions of a metamodel for an industrial-strength object-oriented modeling language, BON. The first version of the metamodel, written in BON itself, is intended to give a precise and understandable description of the syntactic well-formedness constraints. The second version, written in the PVS specification language, is intended to give a formal description of the constraints, in a form that is amenable to automated checking and analysis. We demonstrate how the PVS version can be used for conformance checking, i.e., showing that BON models satisfy or fail to satisfy the metamodel. A process is defined for using the metamodel in carrying out conformance testing of models. We also contrast the BON metamodel with the metamodel of the Unified Modelling Language (UML), both in terms of the precise metamodel presented in the UML Semantics Reference, and a formalization of the metamodel presented in the Alloy specification language. We discuss lessons learned in constructing metamodels, particularly in terms of using the PVS specification language for metamodeling.

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.