MUST: Minimal Unsatisfiable Subsets Enumeration Tool
149
1.8
2
2.2
2.4
2.6
2.8
0
600
1200
1800
2400
3000
3600
average ranking
time in seconds
MUST
MARCO
FLINT
MCSMUS
Fig. 3: Average ranking in time.
The thing is that MUST mostly ranks either as 1st or 2nd on a benchmark and
rarely ranks as 4th, whereas MCSMUS more often ranks as 3rd or 4th.
Finally, let us recall that our tool contains also implementation of the algorithm MARCO and thus one might be interesting in comparing the performance
of MARCO in our tool and MARCO in the tool MARCO. In the SAT domain,
we found our implementation to be more efficient, equal, and less efficient than
MARCO in case of 68, 6, and 26 percent of benchmarks, respectively. In the SMT
domain, our implementation is better, equal, and worse in 37, 29, 34 percent
of benchmarks, respectively
8 . Therefore, shall anyone want to use the algorithm
MARCO, we recommend to use our implementation.
6 Case Study
During the last 4 years, we participated on the European Union’s Horizon 2020
project called AMASS [26]. The project brought together researchers from academia and engineers from large industrial companies such as Honeywell, Alstom,
or Infineon. The project focused on improving the process of development and
certification of Cyber-Physical Systems in markets such as automotive, railway,
aerospace, space, and energy. Among others, this included the development of
techniques for assessing quality of system specification/requirements and this is
where our tool found an application.
Establishing the requirements is an important stage in all development. In
general, the requirements can be expressed either informally, e.g. using a natural
language, or formally by employing a kind of mathematical logic such as the
Linear Temporal Logic (LTL). The formalization removes ambiguity and allows
to employ various model-based techniques, such as model checking. Moreover,
we get the opportunity to verify the requirements earlier, even before any system
model is built. In particular, we can verify that the requirements are consistent
(satisfiable), i.e. that there can be even built a system that satisfies all the
requirements. If the requirements are inconsistent, they need to be refined.
8 See the appendix https://www.fi.muni.cz/%7exbendik/research/must
149
1.8
2
2.2
2.4
2.6
2.8
0
600
1200
1800
2400
3000
3600
average ranking
time in seconds
MUST
MARCO
FLINT
MCSMUS
Fig. 3: Average ranking in time.
The thing is that MUST mostly ranks either as 1st or 2nd on a benchmark and
rarely ranks as 4th, whereas MCSMUS more often ranks as 3rd or 4th.
Finally, let us recall that our tool contains also implementation of the algorithm MARCO and thus one might be interesting in comparing the performance
of MARCO in our tool and MARCO in the tool MARCO. In the SAT domain,
we found our implementation to be more efficient, equal, and less efficient than
MARCO in case of 68, 6, and 26 percent of benchmarks, respectively. In the SMT
domain, our implementation is better, equal, and worse in 37, 29, 34 percent
of benchmarks, respectively
8 . Therefore, shall anyone want to use the algorithm
MARCO, we recommend to use our implementation.
6 Case Study
During the last 4 years, we participated on the European Union’s Horizon 2020
project called AMASS [26]. The project brought together researchers from academia and engineers from large industrial companies such as Honeywell, Alstom,
or Infineon. The project focused on improving the process of development and
certification of Cyber-Physical Systems in markets such as automotive, railway,
aerospace, space, and energy. Among others, this included the development of
techniques for assessing quality of system specification/requirements and this is
where our tool found an application.
Establishing the requirements is an important stage in all development. In
general, the requirements can be expressed either informally, e.g. using a natural
language, or formally by employing a kind of mathematical logic such as the
Linear Temporal Logic (LTL). The formalization removes ambiguity and allows
to employ various model-based techniques, such as model checking. Moreover,
we get the opportunity to verify the requirements earlier, even before any system
model is built. In particular, we can verify that the requirements are consistent
(satisfiable), i.e. that there can be even built a system that satisfies all the
requirements. If the requirements are inconsistent, they need to be refined.
8 See the appendix https://www.fi.muni.cz/%7exbendik/research/must