Detection of Conflicting Compliance Rules

Web-based dynamic systems and pressured business environments need more than ever formal methods to analyze evolving compliance rules. Providing adequate tools to tackle the problem of debugging conflicting temporal compliance rules is an ongoing research topic. This problem is of paramount importance to achieve automatic support for early declarative design and to support evolution of rules in contract-based or service-based systems. In this paper we investigate the problem of extracting temporal unsatisfiable cores in order to detect the inconsistent part of a specification. We survey existing techniques to extract core and provide a new depth-first-search model checking which also enables to extract small unsatisfiable cores.