Metamodelling and Conformance Checking with PVS

  • Richard F. Paige
  • Jonathan S. Ostroff
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2029)


A metamodel expresses the syntactic well-formedness constraints that all models written using the notation of a modelling language must obey. We formally capture the metamodel for an industrial-strength object-oriented modelling language, BON, using the PVS specification language.We discuss how the PVS system helped in debugging the metamodel, and show how to use the PVS theorem prover for conformance checking of models against the metamodel.We consider some of the benefits of using PVS’s specification language, and discuss some lessons learned about formally specifying metamodels.


Modelling Language Inheritance Hierarchy Aggregation Relationship Conformance Check Export Policy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    B. Meyer. Object-Oriented Software Construction, Prentice-Hall, 1997.Google Scholar
  2. 2.
    OMG Unified Modelling Language Specification 1.3, OMG, June 1999.Google Scholar
  3. 3.
    S. Owre, N. Shankar, J. Rushby, and D. Stringer-Calvert. The PVS Language Reference Version 2.3, SRI International Technical Report, September 1999.Google Scholar
  4. 4.
    R. Paige and J. Ostroff.An Object-Oriented Refinement Calculus. Technical Report CS-1999-07, York University, December 1999.Google Scholar
  5. 5.
    R. Paige and J. Ostroff. Precise and Formal Metamodelling with the Business Object Notation and PVS. Technical Report CS-2000-03,York University, August 2000.Google Scholar
  6. 6.
    M. Vaziri and D. Jackson. Some Shortcomings of OCL, the Object Constraint Language of UML. Technical Report, MIT Laboratory for Computer Science, December 1999.Google Scholar
  7. 7.
    K. Walden and J.-M. Nerson. Seamless Object-Oriented Software Development, Prentice-Hall, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Richard F. Paige
    • 1
  • Jonathan S. Ostroff
    • 1
  1. 1.Department of Computer ScienceYork UniversityTorontoCanada

Personalised recommendations