An institution theory of formal meta-modelling in graphically extended BNF

doi:10.1007/s11704-012-2902-4

Front Comput Sci

0, Vol.

Issue () : 40-56 https://doi.org/10.1007/s11704-012-2902-4

RESEARCH ARTICLE

An institution theory of formal meta-modelling in graphically extended BNF

Hong ZHU(

)

Department of Computing and Communication Technologies, Oxford Brookes University, Oxford, UK

Download: PDF(403 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

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.

Keywords meta-modelling modelling languages abstract syntax semantics graphic extension of BNF (GEBNF) formal logic institution

Corresponding Author(s): ZHU Hong,Email:hzhu@brookes.ac.uk

Issue Date: 01 February 2012

Cite this article:

Hong ZHU. An institution theory of formal meta-modelling in graphically extended BNF[J]. Front Comput Sci, 0, (): 40-56.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-012-2902-4
https://academic.hep.com.cn/fcs/EN/Y0/V/I/40

1	Zhu H. On the theoretical foundation of meta-modelling in graphically extended BNF and first order logic. In: Proceedings of the 4th IEEE Symposium on Theoretical Aspects of Software Engineering (TASE’10) , August2010, 95-104
2	Van Lamsweerde A. Formal specification: A roadmap. In: Proceedings of the 22nd International Conference on on Software Engineering - Future of SE Track (ICSE’00), Limerick, Ireland , June2000, 147-159
3	OMG. Meta Object Facility (MOF) 2.0 Core Specification. Technical Report formal/2006-01-01, Object Management Group, Needham, MA 02494, USA , 2006. URL: http://www.omg.org/spec/MOF/2.0
4	OMG. MDA Specification. Object Management Group, Needham, MA 02494, USA , August2010. URL: http://www.omg.org/mda/ specs.htm, Last updated on 08/13/2010
5	OMG. Unified Modeling Language: Superstructure, version 2.0. Technical Report formal/05-07-04, Object Management Group, Needham, MA02494, USA , July2005. URL: http://www.omg.org/spec/UML/2.0
6	France RB, Kim D-K, Ghosh S, Song E. A UML-based pattern specification technique. IEEE Transactions on Software Engineering , 2004, 30(3): 193-206 doi: 10.1109/TSE.2004.1271174
7	Elaasar M, Briand LC, Labiche Y. A metamodeling approach to pattern specification. In: Proceedings of the 9th International Conference on Model Driven Engineering Languages and Systems, (MoDELS’06), Genova, Italy, October 2006, Lecture Notes in Computer Science , 2006, 4199: 484-498 doi: 10.1007/11880240_34
8	Bayley I, Zhu H. Formal specification of the variants and behavioural features of design patterns. Journal of Systems and Software , 2010, 83(2): 209-221 doi: 10.1016/j.jss.2009.09.039
9	Mraidha C, Gerard S, Terrier F, Benzakki J. A two-aspect approach for a clearer behavior model. In: Proceedings of the 6th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC’03) , May2003, 213-220
10	Zhu H, Shan L. Well-formedness, consistency and completeness of graphic models. In: Proceedings of the 9th International Conference on Computer Modelling and Simulation (UKSIM’06), Oxford, UK , April2006, 47-53
11	Bayley I, Zhu H. Specifying behavioural features of design patterns in first order logic. In: Proceedings of the IEEE 32nd International Computer Software and Applications Conference (COMPSAC’08) , 2008, 203-210
12	Zhang Q. Visual software architecture description based on design space. In: Proceedings of The Eighth International Conference on Quality Software (QSIC’08), Oxford, UK , August2008, 366-375
13	Gamma E, Helm R, Johnson R, Vlissides J. Design Patterns-Elements of Reusable Object-Oriented Software. Boston , USA: Addison-Wesley, 1995
14	Zhu H, Bayley I, Shan L, Amphlett R. Tool support for design pattern recognition at model level. In: Proceedings of the 33rd IEEE Annual Conference on Computer Software and Applications (COMPSAC’09), Seattle, Washington, USA , July2009, 228-233
15	Bayley I, Zhu H. On the composition of design patterns. In: Proceedings of the 8th International Conference on Quality Software (QSIC’08), Oxford, UK , August2008, 27-36
16	Bayley I, Zhu H. A formal language of pattern composition. In: Proceedings of the 2nd International Conference on Pervasive Patterns (PATTERNS’10), Lisbon, Portugal , November2010, 1-6
17	Zhu H, Bayley I. Laws of pattern composition. In: Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM’10), Shanghai, China, Lecture Notes in Computer Science , 2010, 6447: 630-645 doi: 10.1007/978-3-642-16901-4_41
18	Goguen J, Burstall R M. Institutions: Abstract model theory for specification and programming. Journal of ACM , 1992, 39(1): 95-146 doi: 10.1145/147508.147524
19	Chiswell I, Hodges W. Mathematical Logic, volume 3 of Oxford Texts in Logic. Oxford University Press , 2007
20	Shan L, Zhu H. Semantics of metamodels in UML. In: Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE’09), Tianjin, China , July2009, 55-62
21	Poernomo I. The meta-object facility typed. In: Proceedings of the 21st Annual ACM Symposium on Applied Computing (SAC’06), Haddad H (eds), Dijon, France , 2006, 1845-1849
22	Boronat A, Meseguer J. An algebraic semantics for MOF. Formal Aspects of Computing , 2010, 22(3-4): 269-296 doi: 10.1007/s00165-009-0140-9
23	Cengarle M V, Knapp A. A formal semantics for OCL 1.4. In: Proceedings of the 4th International Conference on The Unified Modelling Language-Modelling languages, Concepts and Tools (UML’01), Gogalla M, Kobryn C (eds), Lecture Notes in Computer Science , 2001, 2185: 118-133
24	Clarke T, Warmer J. Object Modeling with the OCL: The Rationale behind the Object Constraint Language. Lecture Notes in Computer Science , 2002, 2263
25	Brucker A D, Wolff B. A proposal for a formal OCL semantics in Isabelle/HOL. In: Proceedings of 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’02), Hampton, VA, USA, August 2002, Carreno VA, Munoz CA, Tahar S (eds), Lecture Notes in Computer Science , 2002, 2410: 147-175
26	Flake S. Towards the completion of the formal semantics of OCL 2.0. In: Proceedings of the 27th Australasian Conference on Computer Science (ACSC’04), Darlinghurst, Australia , 2004, 73-82
27	Hennicker R, Knapp A, Baumeister H. Semantics of OCL operation specifications. Electronic Notes in Theoretical Computer Science , November2004, 102: 111-132 doi: 10.1016/j.entcs.2003.09.006
28	Boronat A, Meseguer J. Algebraic semantics of OCL-constrained metamodel specifications. In: Proceedings of the 47th International Conference on Objects, Components, Models and Patterns (TOOLS EUROPE’09), Oriol M, and Meyer B (eds), Zurich, Switzerland, June- July 2009, Lecture Notes in Business Information Processing , 2009, 33: 96-115
29	Boronat A, Meseguer J. Algebraic semantics of EMOF/OCL metamodels. Technical Report UIUCDCS-R-2007-2904, Department of Computer Science, University of Illinois at Urbana-Champaign, USA , October2007. URL: http://hdl.handle.net/2142/11398; Accessed on 5 Feb. 2010
30	Brucker A D, Doser J, Wolff B. Semantic issues of OCL: Past, present, and future. In: Proceedings of the 6th OCL Workshop at UML/MoDELS’06 , 2006, 213-228
31	Eden A H. Formal specification of object-oriented design. In: Proceedings of the International Conference on Multidisciplinary Design in Engineering, Montreal, Canada , November2001
32	Gasparis E, Nicholson J, Eden A H. LePUS3: An object-oriented design description language. In: Proceedings of the 5th International Conference on Diagrammatic Representation and Inference (Diagrams’ 08), Herrsching, Germany, September 2008, Lecture Notes in Computer Science , 2008, 5223: 364-367 doi: 10.1007/978-3-540-87730-1_37
33	Maplesden D, Hosking J, Grundy J. A visual language for design pattern modelling and instantiation. In: Proceedings of 2001 IEEE CS International Symposium on Human-Centric Computing Languages and Environments (HCC’01), Stresa, Italy , September2001, 338-339
34	Maplesden D, Hosking J, Grundy J. Design pattern modelling and instantiation using DPML. In: Proceedings of the Fortieth International Conference on Tools Pacific (TOOLS Pacific’02), Darlinghurst, Australia , 2002, 3-11
35	Albin-Amiot H, Cointe P, Guéhéneuc Y, Jussien N. Instantiating and detecting design patterns: Putting bits and pieces together. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE’01), San Diego, CA, USA , November2001, 166-173

[1]	Yamin HU, Hao JIANG, Zongyao HU. Measuring code maintainability with deep neural networks[J]. Front. Comput. Sci., 2023, 17(6): 176214-.
[2]	Fanchao QI, Ruobing XIE, Yuan ZANG, Zhiyuan LIU, Maosong SUN. Sememe knowledge computation: a review of recent advances in application and expansion of sememe knowledge bases[J]. Front. Comput. Sci., 2021, 15(5): 155327-.
[3]	Thierry GAUTIER, Clément GUY, Alexandre HONORAT, Paul LE GUERNIC, Jean-Pierre TALPIN, Loïc BESNARD. Polychronous automata and their use for formal validation of AADL models[J]. Front. Comput. Sci., 2019, 13(4): 677-697.
[4]	Ying JIANG, Shichao LIU, Thomas EHRHARD. A fully abstract semantics for value-passing CCS for trees[J]. Front. Comput. Sci., 2019, 13(4): 828-849.
[5]	Xiao PAN,Weizhang CHEN,Lei WU,Chunhui PIAO,Zhaojun HU. Protecting personalized privacy against sensitivity homogeneity attacks over road networks in mobile services[J]. Front. Comput. Sci., 2016, 10(2): 370-386.
[6]	Yang ZHANG,Xinyu FENG. An operational happens-before memory model[J]. Front. Comput. Sci., 2016, 10(1): 54-81.
[7]	Yanhong HUANG,Jifeng HE,Huibiao ZHU,Yongxin ZHAO,Jianqi SHI,Shengchao QIN. Semantic theories of programs with nested interrupts[J]. Front. Comput. Sci., 2015, 9(3): 331-345.
[8]	Xiaoxiao YANG,Yu ZHANG,Ming FU,Xinyu FENG. A temporal programming model with atomic blocks based on projection temporal logic[J]. Front. Comput. Sci., 2014, 8(6): 958-976.
[9]	Qin LI, Yongxin ZHAO, Huibiao ZHU, Jifeng HE. A UTP semantic model for Orc language with execution status and fault handling[J]. Front. Comput. Sci., 2014, 8(5): 709-725.
[10]	Zengchang QIN, Tao WAN. Hybrid Bayesian estimation tree learning with discrete and fuzzy labels[J]. Front Comput Sci, 2013, 7(6): 852-863.
[11]	Zhibin YANG, Jean-Paul BODEVEIX, Mamoun FILALI. A comparative study of two formal semantics of the SIGNAL language[J]. Front Comput Sci, 2013, 7(5): 673-693.
[12]	Shuling WANG, Qin SHU, Yijing LIU, Zongyan QIU, . A semantic model of confinement and Locality Theorem[J]. Front. Comput. Sci., 2010, 4(1): 28-46.
[13]	HE Jifeng, ZHU Huibiao, PU Geguang. A model for BPEL-like languages[J]. Front. Comput. Sci., 2007, 1(1): 9-19.

Viewed

Full text

Abstract

Cited

Shared

Discussed