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

Hong ZHU

PDF(403 KB)
PDF(403 KB)
Front. Comput. Sci. ›› DOI: 10.1007/s11704-012-2902-4
RESEARCH ARTICLE

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

Author information +
History +

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

Cite this article

Download citation ▾
Hong ZHU. An institution theory of formal meta-modelling in graphically extended BNF. Front Comput Sci, https://doi.org/10.1007/s11704-012-2902-4

References

[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), <month>August</month>2010, 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, <month>June</month>2000, 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, <month>August</month>2010. 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, <month>July</month>2005. 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
CrossRef Google scholar
[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
CrossRef Google scholar
[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
CrossRef Google scholar
[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), <month>May</month>2003, 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, <month>April</month>2006, 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, <month>August</month>2008, 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, <month>July</month>2009, 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, <month>August</month>2008, 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, <month>November</month>2010, 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
CrossRef Google scholar
[18]
Goguen J, Burstall R M. Institutions: Abstract model theory for specification and programming. Journal of ACM, 1992, 39(1): 95-146
CrossRef Google scholar
[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, <month>July</month>2009, 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
CrossRef Google scholar
[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, <month>November</month>2004, 102: 111-132
CrossRef Google scholar
[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, <month>October</month>2007. 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, <month>November</month>2001
[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
CrossRef Google scholar
[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, <month>September</month>2001, 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, <month>November</month>2001, 166-173

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg
AI Summary AI Mindmap
PDF(403 KB)

Accesses

Citations

Detail

Sections
Recommended

/