Formal Foundations of Consistency in Model-Driven Development

Models are abstractions used to precisely represent specific aspects of a system in order to make work easier for engineers. This separation of concerns naturally leads to a proliferation of models, and thus to the challenge of ensuring that all models actually represent the same system. We can study this problem by considering that the property is abstracted as a relation between models called consistency. Yet, the exact nature of this relation remains unclear in the context of cyber-physical systems, as such models are heterogeneous and may not be formally described. Therefore, we propose a formal foundation for consistency relations, by (1) providing a set-theoretical description of the virtual single underlying model (V-SUM) methodology, (2) relating consistency to model transformations, and (3) studying the connection between consistency of models and their semantics. In particular, we show that a relation on the semantic spaces of models can be reflected as a relation on models and that this semantics forms a lattice, such that a canonical semantics can be derived from a consistency relation. Our findings lay the foundation for a formal reasoning about precise notions of consistency.