Consistency Checking in Requirements Analysis

Investor logo


This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on


BENDÍK Jaroslav

Year of publication 2017
Type Article in Proceedings
Conference Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2017
MU Faculty or unit

Faculty of Informatics

Field Informatics
Keywords Requirements analysis; Consistency; Minimal inconsistent subsets
Description In the last decade it became a common practise to formalise software requirements using a mathematical language of temporal logics, e.g., LTL. The formalisation removes ambiguity and improves understanding. Formal description also enables various model-based techniques, like formal verification. Moreover, we get the opportunity to check the requirements earlier, even before any system model is built. This so called requirements sanity checking aims to assure that a given set of requirements is consistent, i.e., that a product satisfying all the requirements can be developed. If inconsistencies are found, it is desirable to present them to the user in a minimal fashion, exposing the core problems among the requirements. Such cores are called minimal inconsistent subsets (MISes). In this work, we present a framework for online MISes enumeration in the domain of temporal logics.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.