Repairing Conformance Violations with a Reference Model in the Context of Automata Decomposition
ACM/IEEE International Conference on Model Driven Engineering Languages and Systems (MODELS), pp. 835–844
Abstract
Existing conformance-checking approaches typically compare a reference model with a monolithic concrete model and therefore do not support decompositions into interacting subcomponents. We present a conformance-checking and repair approach for time-synchronous component-and-connector subarchitectures with statechart-based component behavior. Given a reference component, a concrete cascade composition with delayed feedback, and an incarnation mapping, the approach checks whether the composition’s observable behavior conforms to the reference. On failure, it returns a counterexample, localizes the violation to the responsible subcomponent and repair site, and synthesizes a repair via MaxSMT, minimizing syntactic change, bounded behavioral loss, and distance from the blamed component. Re-checking validates each repair. Experiments with seeded faults and generated composition chains show accurate localization and conformance-restoring repairs, with repair synthesis dominating runtime.
Authors 7
-
Karlsruhe Institute of Technology
Affiliation as printed
Karlsruhe Institute of Technology, Karlsruhe, Germany
-
Max Stachon Aachen
Affiliation as printed
RWTH Aachen University, Aachen, Germany
-
Adrian Marin Aachen
Affiliation as printed
RWTH Aachen University, Aachen, Germany
-
Affiliation as printed
Ulm University, Ulm, Germany
-
Bernhard Rumpe⋆ Aachen
Affiliation as printed
RWTH Aachen University, Aachen, Germany
-
Karlsruhe Institute of Technology
Affiliation as printed
Karlsruhe Institute of Technology, Karlsruhe, Germany
-
Affiliation as printed
Ulm University, Ulm, Germany
Cited by 0 stored of 0
No patents citing this paper on Lens.org (checked 2026-10-11).