Fault localization in DSLTrans model transformations by combining symbolic execution and spectrum-based analysis.

Area of Science:

• Software Engineering
• Model-Driven Engineering
• Formal Methods

Background:

• Model transformation verification is crucial for robust model-driven engineering and automated quality assurance.
• Existing contract checking methods efficiently detect property violations but struggle with precise fault localization.
• Current fault localization techniques require burdensome test case creation and maintenance.

Purpose of the Study:

• To develop a fault localization approach for identifying faulty rules in DSLTrans model transformations.
• To combine symbolic execution with spectrum-based fault localization, eliminating the need for test input models.
• To evaluate the effectiveness of this combined approach for improving model transformation verification.

Main Methods:

• Employs symbolic execution to verify model transformations and evaluate contract satisfaction.
• Utilizes the path condition output from symbolic execution for fault localization.
• Applies spectrum-based analysis techniques to track and rank faulty transformation rules.

Main Results:

• The best spectrum-based analysis techniques achieved an average EXAM score below 0.30, indicating high localization efficiency.
• The approach successfully located the faulty rule within the top-three ranked rules in 70% of evaluated cases.
• Analysis covered the impact of transformation complexity, mutation type, and contract type on localization accuracy.

Conclusions:

• Combining symbolic execution with spectrum-based fault localization offers an effective, test-case-free method for identifying faulty model transformation rules.
• The proposed technique significantly reduces the effort required for debugging model transformations.
• Further investigation into limitations and potential pre-checks is recommended for broader applicability.