Evaluating Coverage and Fault Detection Capability of Scenario-Based Validation of Asmeta Specifications

Scenario-based validation is a widely used technique for assessing the correctness of executable formal specifications, yet its effectiveness strongly depends on the adequacy of the scenarios used. Coverage measures have been commonly adopted to evaluate scenario adequacy, but it remains unclear whether higher coverage correlates with improved fault detection, especially at the level of formal specifications. While this relationship has been extensively studied for source code, it has received little attention in the context of executable formal models. In this paper, we investigate the relationship between coverage and fault detection capability for scenario-based validation of Asmeta specifications. We extend the AsmetaV tool with an extensive set of coverage criteria that go beyond existing macro rule coverage. To assess the effectiveness of these coverage criteria, we introduce a set of mutation operators for Asmeta specifications and conduct a large-scale mutation-based experimental study, based on scenarios generated through model-checking-based, random, and evolutionary techniques. Our results show that higher coverage is generally correlated with increased fault detection capability, but macro rule coverage alone is insufficient to capture scenario effectiveness and more fine-grained coverage criteria provide stronger correlation with mutation scores and lead to improved fault detection.