A theoretic framework of bidirectional transformation between systems and models

Synchronization between systems and models has been explored in model-driven engineering to enable model-based system management. Despite its promising use, there is a lack of a theoretic foundation for state-based system-model synchronization. This paper proposes a theory for state-based system-model bidirectional transformation (BX), and defines seven combinators for system-model BX to facilitate the development of well-behaved synchronizer programs. A system-model BX is a single program that converts a system with a model consistently. Forwards, it creates a model according to a system as a conventional BX. Backwards, it generates a set of system edits, which can turn the current system into a new state that is consistent with the given model. System-model BX is fully aware of the domain constraints about how to change a system, and plans a reasonable execution order for those edits, rather than applying them blindly. The paper also demonstrates the use of system-model BX by building a generic system-model synchronizer and a concrete file system synchronizer.