Consistency Verification of Specification Rules

摘要

This paper focuses on the consistency analysis of specification rules expressing relationships between input and expected output of systems. We identified the link between Minimal Inconsistent Sets (MISes) of rules and Minimal Unsatisfiable Subsets (MUSes) of constraints. For practical consistency verification of rules, we developed a novel algorithm using SMT solvers for fast enumeration of MUSes. We evaluated the algorithm using publicly available benchmarks. Finally, we used the approach to verify the consistency of specifications rules extracted from real-world case studies.