Formal Foundations of Consistency in Model-Driven Development

Here is a link to the publication.

The ISoLA Symposium is a forum for developers, users, and researchers to discuss issues related to the adoption and use of rigorous tools for the specification, analysis, verification, certification, construction, test, and maintenance of systems from the point of view of their different application domains. To bridge the gap between designers and developers of (formal methods based) rigorous tools, and users in engineering and in other disciplines, it fosters and exploits synergetic relationships among scientists, engineers, software developers, decision makers, and other critical thinkers.

Abstract : 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) item 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 space 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.