CoCoPath: Concolic Exploration of Consistency-Preserving Paths

Maintaining consistency between related models is achieved through Consistency Preservation Rules (CPRs) that propagate changes from a source model to a target model. However, in many cases, additional input from the maintainer of a target model, based on their domain knowledge, is required to integrate changes into target models. Therefore, the change cannot be propagated automatically and introduces temporary inconsistency. To manage the temporary inconsistency, we propose CoCoPath, a concolic execution framework for systematically exploring execution paths in consistency-preserving model transformations. We combine dynamic taint tracking, concolic execution, and model transformation frameworks to derive potential target models based on the source model, the consistency preservation rules, and optional domain constraints to further restrict the search space. By comparing these alternative target models, users can explore the consequences of different additional inputs and resolve temporary inconsistency in an informed manner. We validate our contribution by applying our approach to an industry case study, showcasing its capabilities for one and multiple awaited user inputs.