An institution theory of formal meta-modelling in graphically extended BNF
Hong ZHU
An institution theory of formal meta-modelling in graphically extended BNF
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.
meta-modelling / modelling languages / abstract syntax / semantics / graphic extension of BNF (GEBNF) / formal logic / institution
[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
|
/
〈 | 〉 |