# Formalizing Cyber--Physical System Model Transformation via Abstract Interpretation

## TL;DR

This paper introduces a formal, sound approach to model transformation in cyber-physical systems using abstract interpretation, enabling consistent and domain-agnostic system modeling.

## Contribution

It develops a foundational methodology for model transformation based on abstract interpretation, with formal proofs of correctness and domain transfer capabilities.

## Key findings

- Proves soundness of the abstract interpretation-based transformation
- Defines formalism for encoding model properties
- Demonstrates cross-domain applicability of the approach

## Abstract

Model transformation tools assist system designers by reducing the labor--intensive task of creating and updating models of various aspects of systems, ensuring that modeling assumptions remain consistent across every model of a system, and identifying constraints on system design imposed by these modeling assumptions. We have proposed a model transformation approach based on abstract interpretation, a static program analysis technique. Abstract interpretation allows us to define transformations that are provably correct and specific. This work develops the foundations of this approach to model transformation. We define model transformation in terms of abstract interpretation and prove the soundness of our approach. Furthermore, we develop formalisms useful for encoding model properties. This work provides a methodology for relating models of different aspects of a system and for applying modeling techniques from one system domain, such as smart power grids, to other domains, such as water distribution networks.