Metamodelling and Conformance Checking with PVS

Research output: Contribution to conferencePaper



Publication details

DatePublished - 2001
Number of pages14
Original languageUndefined/Unknown


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.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations