×

zbMATH — the first resource for mathematics

An institution theory of formal meta-modelling in graphically extended BNF. (English) Zbl 1251.68080
Summary: Meta-modelling plays an important role in model driven software development. In this paper, a graphic extension of BNF (GEBNF) is proposed to define the abstract syntax of graphic modelling languages. From a GEBNF syntax definition, a formal predicate logic language can be induced so that meta-modelling can be performed formally by specifying a predicate on the domain of syntactically valid models. In this paper, we investigate the theoretical foundation of this meta-modelling approach. We formally define the semantics of GEBNF and its induced predicate logic languages, then apply Goguen and Burstall’s institution theory to prove that they form a sound and valid formal specification language for meta-modelling.
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
HOL-OCL
PDF BibTeX XML Cite
Full Text: DOI