Metamodelling and Conformance Checking with PVS

Richard F. Paige, Jonathan S. Ostroff

Research output: Contribution to conferencePaperpeer-review


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.
Original languageUndefined/Unknown
Number of pages14
Publication statusPublished - 2001

Cite this