Consistency Checking in Requirements Analysis

BENDÍK, Jaroslav. Consistency Checking in Requirements Analysis. Online. In Tevfik Bultan, Koushik Sen. Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2017. 26th ed. NY, USA: ACM New York, 2017, p. 408-411. ISBN 978-1-4503-5076-1. Available from: https://dx.doi.org/10.1145/3092703.3098239.

Basic information

• Original name: Consistency Checking in Requirements Analysis
• Authors: BENDÍK, Jaroslav (203 Czech Republic, guarantor, belonging to the institution).
• Edition: 26. vyd. NY, USA, Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2017, p. 408-411, 4 pp. 2017.
• Publisher: ACM New York

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: United States of America
• Confidentiality degree: is not subject to a state or trade secret
• Publication form: electronic version available online
• RIV identification code: RIV/00216224:14330/17:00097173
• Organization unit: Faculty of Informatics
• ISBN: 978-1-4503-5076-1
• Doi: http://dx.doi.org/10.1145/3092703.3098239
• UT WoS: 000462903600046
• Keywords in English: Requirements analysis; Consistency; Minimal inconsistent subsets
• Tags: International impact, Reviewed

Abstract

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.

Links

• MUNI/A/0897/2016, interní kód MU: Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.

Investor: Masaryk University, Category A

• 692474, interní kód MU: Name: AMASS - Architecture-driven, Multi-concern and Seamless Assurance and Certification of Cyber-Physical Systems (Acronym: AMASS)

Investor: European Union, ECSEL