A Formal Embedding for Assessing the Complexity of Model Consistency

Modeling and model-driven processes offer abstraction to cope with the increasing complexity of systems. Since federated models describe overlapping aspects of the same system, some information is shared, introducing redundancy. Maintaining consistency of such information is crucial to ensure a coherent system representation. In safety-critical domains, such consistency requirements often require formal verification to ensure strong correctness guarantees. However, the verification effort is influenced not only by the models themselves, but also by the structure and expressiveness of the consistency specifications. In this article, we examine the complexity of consistency from a formal perspective. We embed OCL-based consistency constraints into higher-order logic using the theorem prover Isabelle/HOL and analyze the resulting proof obligations. By identifying key dimensions that influence the verification effort, we aim to understand how the design of consistency specifications affects the formal reasoning required to assess them. We illustrate the approach via a case study of a car braking system, for which we construct a mechanized formalization of realistic metamodels and consistency constraints, and discuss metrics for their proof complexity. ... mehrUnderstanding which structural aspects of consistency influence the verification effort provides a foundation for ultimately reducing unnecessary complexity while ensuring the required consistency constraint.