Repairing Conformance Violations with a Reference Model in the Context of Automata Decomposition

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.