Reasoning about Metamodeling with Formal Specifications and Automatic Proofs

详细信息    查看全文

• 作者：Ethan K. Jackson (1) ejackson@microsoft.com
  Tihamér Levendovszky (2) tihamer@isis.vanderbilt.edu
  Daniel Balasubramanian (2) daniel@isis.vanderbilt.edu
• 刊名：Lecture Notes in Computer Science
• 出版年：2011
• 出版时间：2011
• 年：2011
• 卷：6981
• 期：1
• 页码：653-667
• 全文大小：249.9 KB
• 参考文献：1. Clark, T., Evans, A., Caskurlu, B.: The Meta-modeling Language Calculus: Foundation Semantics for UML. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 17–31. Springer, Heidelberg (2001)
  2. Jouault, F., Bézivin, J.: KM3: A DSL for Metamodel Specification. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 171–185. Springer, Heidelberg (2006)
  3. Varró, D., Pataricza, A.: VPM: A visual, precise and multilevel metamodeling framework for describing mathematical domains and UML. Journal of Software and Systems Modeling 2(3), 187–210 (2003)
  4. Alanen, M., Porres, I.: A Metamodeling Language Supporting Subset and Union Properties. Software and System Modeling 7(1), 103–124 (2008)
  5. Boronat, A., Meseguer, J.: An Algebraic Semantics for MOF. Formal Asp. Comput. 22(3-4), 269–296 (2010)
  6. Jackson, E.K., Kang, E., Dahlweid, M., Seifert, D., Santen, T.: Components, platforms and possibilities: towards generic automation for MDA. In: EMSOFT, pp. 39–48 (2010)
  7. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation (Monographs in Theoretical Computer Science). An EATCS Series. Springer-Verlag New York, Inc., Secaucus (2006)
  8. Atkinson, C., Kühne, T.: The Essence of Multilevel Metamodeling. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, pp. 19–33. Springer, Heidelberg (2001)
  9. Dantsin, E., Eiter, T., Gottlob, G., Voronkov, A.: Complexity and expressive power of logic programming. ACM Comput. Surv. 33(3), 374–425 (2001)
  10. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and Programming in Rewriting Logic. Theor. Comput. Sci. 285(2), 187–243 (2002)
  11. Varró, D.: Automated Formal Verification of Visual Modeling Languages by Model Checking. Software and System Modeling 3(2), 85–113 (2004)
  12. Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: A Challenging Model Transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436–450. Springer, Heidelberg (2007)
  13. Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)
  14. Ehrig, K., Küster, J.M., Taentzer, G.: Generating Instance Models From Meta Models. Software and System Modeling 8(4), 479–500 (2009)
  15. Gr?nniger, H., Ringert, J.O., Rumpe, B.: System Model-Based Definition of Modeling Language Semantics. In: FMOODS/FORTE, pp. 152–166 (2009)
  16. Mendon?a, M., Wasowski, A., Czarnecki, K.: SAT-based Analysis of Feature Models is Easy. In: SPLC, pp. 231–240 (2009)
  17. Jackson, E.K., Sztipanovits, J.: Constructive Techniques for Meta- and Model-Level Reasoning. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 405–419. Springer, Heidelberg (2007)
  18. Jaffar, J., Maher, M.J., Marriott, K., Stuckey, P.J.: The Semantics of Constraint Logic Programs. J. Log. Program. 37(1-3), 1–46 (1998)
  19. de Moura, L., Bj?rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
  20. Object Management Group: Meta Object Facility (MOF) Core Specification Version 2.4 (2010)
• 作者单位：1. Microsoft Research, Redmond, WA, USA2. Vanderbilt University, Nashville, TN, USA
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

Metamodeling is foundational to many modeling frameworks, and so it is important to formalize and reason about it. Ideally, correctness proofs and test-case generation on the metamodeling framework should be automatic. However, it has yet to be shown that extensive automated reasoning on metamodeling frameworks can be achieved. In this paper we present one approach to this problem: Metamodeling frameworks are specified modularly using algebraic data types and constraint logic programming (CLP). Proofs and test-case generation are encoded as CLP satisfiability problems and automatically solved.