Metamodelling and Conformance Checking with PVS

Richard F. Paige; Jonathan S. Ostroff

doi:10.1007/3-540-45314-8_2

Metamodelling and Conformance Checking with PVS

Richard F. Paige, Jonathan S. Ostroff

Computer Science

Research output: Contribution to conference › Paper › peer-review

Abstract

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 language	Undefined/Unknown
Pages	2-16
Number of pages	14
DOIs	https://doi.org/10.1007/3-540-45314-8_2
Publication status	Published - 2001

Access to Document

10.1007/3-540-45314-8_2

http://link.springer.de/link/service/series/0558/bibs/2029/20290002.htm

Cite this

@conference{103c187150434500836b5d635433255a,

title = "Metamodelling and Conformance Checking with PVS",

abstract = "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{\textquoteright}s specification language, and discuss some lessons learned about formally specifying metamodels. ",

author = "Paige, {Richard F.} and Ostroff, {Jonathan S.}",

year = "2001",

doi = "10.1007/3-540-45314-8_2",

language = "Undefined/Unknown",

pages = "2--16",

}

TY - CONF

T1 - Metamodelling and Conformance Checking with PVS

AU - Paige, Richard F.

AU - Ostroff, Jonathan S.

PY - 2001

Y1 - 2001

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-45314-8_2

DO - 10.1007/3-540-45314-8_2

M3 - Paper

SP - 2

EP - 16

ER -