Abstract
The structural semantics of UML-based metamodeling were recently explored[1], providing a characterization of the models adhering to a metamodel. In particular, metamodels can be converted to a set of constraints expressed in a decidable subset of first-order logic, an extended Horn logic. We augment the constructive techniques found in logic programming, which are also based on an extended Horn logic, to produce constructive techniques for reasoning about models and metamodels. These methods have a number of practical applications: At the meta-level, it can be decided if a (composite) metamodel characterizes a non-empty set of models, and a member can be automatically constructed. At the model-level, it can be decided if a submodel has an embedding in a well-formed model, and the larger model can be constructed. This amounts to automatic model construction from an incomplete model. We describe the concrete algorithms for constructively solving these problems, and provide concrete examples.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Jackson, E.K., Sztipanovits, J.: Towards a formal foundation for domain specific modeling languages. In: EMSOFT 2006. Proceedings of the Sixth ACM International Conference on Embedded Software, pp. 53–62. ACM Press, New York (2006)
Object Management Group: Meta object facility specification v1.4. Technical report (2002)
Object Management Group: Unified modeling language: Superstructure version 2.0, 3rd revised submission to omg rfp. Technical report (2003)
Drewes, F., Hoffmann, B., Plump, D.: Hierarchical graph transformation. J. Comput. Syst. Sci. 64(2), 249–283 (2002)
Ehrig, H., Prange, U., Taentzer, G.: Fundamental theory for typed attributed graph transformation. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 161–177. Springer, Heidelberg (2004)
Burris, S.N., Sankappanavar, H.: A Course in Universal Algebra. Springer, Heidelberg (1981)
Dantsin, E., Eiter, T., Gottlob, G., Voronkov, A.: Complexity and expressive power of logic programming. ACM Comput. Surv. 33(3), 374–425 (2001)
Minker, J.: Logic and databases: A 20 year retrospective. In: Logic in Databases, pp. 3–57 (1996)
Chan, D.: Constructive negation based on the complete database. In: Proc. Int. Conference on LP 1988, pp. 111–125. MIT Press, Cambridge (1988)
Emerson, M., Sztipanovits, J.: Techniques for metamodel composition. In: OOPSLA 2006 Domain-Specific Languages Workshop (2006)
Csertan, G., Huszerl, G., Majzik, I., Pap, Z., Pataricza, A., Varro, D.: Viatra: Visual automated transformations for formal verification and validation of uml models (2002)
Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM 50(1), 63–69 (2003)
Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: ICLP/SLP, pp. 1070–1080 (1988)
Karsai, G., Sztipanovits, J., Ledeczi, A., Bapty, T.: Model-integrated development of embedded software. Proceedings of the IEEE 91, 145–164 (2003)
Karsai, G., Agrawal, A., Shi, F.: On the use of graph transformations for the formal specification of model interpreters. Journal of Universal Computer Science 9(11), 1296–1321 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jackson, E.K., Sztipanovits, J. (2007). Constructive Techniques for Meta- and Model-Level Reasoning. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds) Model Driven Engineering Languages and Systems. MODELS 2007. Lecture Notes in Computer Science, vol 4735. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75209-7_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-75209-7_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75208-0
Online ISBN: 978-3-540-75209-7
eBook Packages: Computer ScienceComputer Science (R0)