150
J. Bend´ ık and I. ˇ
Cern´ a
requirements
expressed in a natural
language
set C of requirements
expressed in a
temporal logic
formalization
consistency
check
inconsistent
MUS enumeration tool
a set K of MUSes of C
consistent
enumerating several
MUSes of C
refining C
based on K
Fig. 4: Application of MUS enumeration in requirements analysis.
Within the AMASS project, we proposed a scheme [6] that exploits MUSes
to help the user to establish a consistent set of requirements. A basic workflow
of the scheme is depicted in Fig. 4. The process starts by introducing a set of
requirements in some natural-language like format, yet using a restricted grammar that avoids ambiguities. In the next step, the requirements are formalized
using LTL and gathered in a set C. Subsequently, C is checked for consistency. If
C is consistent, then the software development process can continue with a next
stage. Otherwise, a MUS enumeration tool is used to identify a set K of MUSes
of C, and the user uses K to refine C. The MUS identification and refinement
steps are repeated until the set of requirements becomes consistent.
We implemented the scheme in AMASS as a part of a so-called V&V manager [27]: a tool for validation and verification of the system model and system
requirements. Our industrial partners employed the scheme on a set of industrial
benchmarks, and evaluated two contemporary MUS enumeration tools from the
LTL domain: our MUST, and Looney by Bauch et al. [4]. They found MUST to be
faster by several orders of magnitude. Unfortunately, the industrial benchmarks
are confidential and cannot be published in this paper. Yet, authors of Looney
indeed acknowledge in their paper that Looney can handle only small input constraint sets containing just low tens of constraints. On the other hand, MUST was
shown [8] to be able to efficiently work with hundreds of constraints.
7 Conclusion
We presented a tool, called MUST, for online enumeration of Minimal Unsatisfiable Subsets (MUSes). MUST implements three contemporary domain agnostic
MUS enumeration algorithms, i.e. algorithms that can be applied in any constraint domain. Currently, the tool supports enumeration in the SAT, SMT and
LTL domains, and can be easily extended to support another domains. Therefore,
we classify the tool itself as domain agnostic; it serves as (an almost) ready-touse solution for any domain where MUSes already find or eventually will find
an application. We experimentally compared MUST to a domain agnostic tool
by Liffiton et al. [22] in the SAT and SMT domains, and we showed that MUST
conclusively dominates in both domains. Moreover, we showed that MUST is
even competitive to contemporary tools that are tailored for the SAT domain.
J. Bend´ ık and I. ˇ
Cern´ a
requirements
expressed in a natural
language
set C of requirements
expressed in a
temporal logic
formalization
consistency
check
inconsistent
MUS enumeration tool
a set K of MUSes of C
consistent
enumerating several
MUSes of C
refining C
based on K
Fig. 4: Application of MUS enumeration in requirements analysis.
Within the AMASS project, we proposed a scheme [6] that exploits MUSes
to help the user to establish a consistent set of requirements. A basic workflow
of the scheme is depicted in Fig. 4. The process starts by introducing a set of
requirements in some natural-language like format, yet using a restricted grammar that avoids ambiguities. In the next step, the requirements are formalized
using LTL and gathered in a set C. Subsequently, C is checked for consistency. If
C is consistent, then the software development process can continue with a next
stage. Otherwise, a MUS enumeration tool is used to identify a set K of MUSes
of C, and the user uses K to refine C. The MUS identification and refinement
steps are repeated until the set of requirements becomes consistent.
We implemented the scheme in AMASS as a part of a so-called V&V manager [27]: a tool for validation and verification of the system model and system
requirements. Our industrial partners employed the scheme on a set of industrial
benchmarks, and evaluated two contemporary MUS enumeration tools from the
LTL domain: our MUST, and Looney by Bauch et al. [4]. They found MUST to be
faster by several orders of magnitude. Unfortunately, the industrial benchmarks
are confidential and cannot be published in this paper. Yet, authors of Looney
indeed acknowledge in their paper that Looney can handle only small input constraint sets containing just low tens of constraints. On the other hand, MUST was
shown [8] to be able to efficiently work with hundreds of constraints.
7 Conclusion
We presented a tool, called MUST, for online enumeration of Minimal Unsatisfiable Subsets (MUSes). MUST implements three contemporary domain agnostic
MUS enumeration algorithms, i.e. algorithms that can be applied in any constraint domain. Currently, the tool supports enumeration in the SAT, SMT and
LTL domains, and can be easily extended to support another domains. Therefore,
we classify the tool itself as domain agnostic; it serves as (an almost) ready-touse solution for any domain where MUSes already find or eventually will find
an application. We experimentally compared MUST to a domain agnostic tool
by Liffiton et al. [22] in the SAT and SMT domains, and we showed that MUST
conclusively dominates in both domains. Moreover, we showed that MUST is
even competitive to contemporary tools that are tailored for the SAT domain.