Formal Foundations of Consistency in Model-Driven Development

@InProceedings{PascualBeckertUlbrichKirstenPfeifer2024,
  title        = {Formal Foundations of Consistency in Model-Driven Development},
  author       = {Romain Pascual and
                  Bernhard Beckert and
                  Mattias Ulbrich and
                  Michael Kirsten and
                  Wolfram Pfeifer},
  year         = {2024},
  month        = oct,
  booktitle    = {12th International Symposium on Leveraging Applications of Formal Methods,
                  Verification and Validation ({ISoLA} 2024).
                  Specification and Verification},
  pages        = {178--200},
  venue        = {Hersonissos, Greece},
  eventdate    = {2024-10-27/2024-10-31},
  series       = {Lecture Notes in Computer Science},
  volume       = {15222},
  part         = {Part {III}},
  publisher    = {Springer},
  editor       = {Tiziana Margaria and
                  Bernhard Steffen},
  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) 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.},
  doi          = {10.1007/978-3-031-75380-0_11}
}