B model quality assessments on automated reachability repair with ISO/IEC 25010

In software engineering, formal methods are often used to specify and verify design models of software products. Whether design models are consistent with required properties can significantly impact the quality of final software products. In this work, we study B model quality measurements based on the ISO/IEC 25010 standard. These measurements are formulated as domain-independent formulae and computed by model checking. Moreover, we study how to enable machines to automatically solve unreachable goals in B models. We suggest to use constraint solvers and semantic learners to discover state transitions to the goals. To demonstrate the effectiveness of the model repair technique, a set of experiments are conducted based on the model quality measurements. The results demonstrate that the model repair technique can solve unreachable goals while preserving the quality of models.