Consistency Verification of Specification Rules (Abstract)

Abstract. This paper focuses on the consistency analysis of specifica- tion 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 con- straints. 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.

Keywords:Specification rules, Consistency verification, Minimal Inconsistent Sets (MISes), Minimal Unsatisfiable Subsets (MUSes), SMTs.