Zhu, Hong An institution theory of formal meta-modelling in graphically extended BNF. (English) Zbl 1251.68080 Front. Comput. Sci. 6, No. 1, 40-56 (2012). 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.) Keywords:meta-modelling; modelling languages; abstract syntax; semantics; graphic extension of BNF (GEBNF); formal logic; institution Software:HOL-OCL PDF BibTeX XML Cite \textit{H. Zhu}, Front. Comput. Sci. 6, No. 1, 40--56 (2012; Zbl 1251.68080) Full Text: DOI