Constructive Techniques for Meta- and Model-Level Reasoning

TitleConstructive Techniques for Meta- and Model-Level Reasoning
Publication TypeConference Paper
Year of Publication2007
AuthorsJackson, E., and J. Sztipanovits
Conference NameModels'07
Date Published10/2007
Conference LocationNashville, TN

The structural semantics of UML-based metamodeling were
recently explored, 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
embeddeding 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.

jackson_MODELS07.pdf256.29 KB