一句话：提出变异模型检测，利用变异体评估形式规约强度并自动强化规约，使其能排除故障变异体。
模型检测依赖形式规约来刻画系统应满足的性质，但规约可能过弱，无法发现模型中的故障。本文提出变异模型检测（mutation model checking）：借鉴变异测试思想，对模型进行有意的变异，并用原规约检查这些变异体；若规约不能检测出变异体，则说明规约强度不足。作者在两个案例研究上进行初步实验，发现原规约仅能检测 40% 和 60% 的随机生成变异体，证实了该问题的现实性。为此，论文提出一个框架来强化原始规约，使得原模型仍然满足强化后的规约，而变异体不再满足，从而提升模型检测中形式规约的故障检测能力。
We propose mutation model checking as an approach to strengthen formal specifications used for model checking. Inspired by mutation testing, our approach concludes that specifications are not strong enough if they fail to detect faults in purposely mutated models. Our preliminary experiments on two case studies confirm the relevance of the problem: their specification can only detect 40% and 60% of randomly generated mutants. As a result, we propose a framework to strengthen the original specification, such that the original model satisfies the strengthened specification but the mutants do not.