Is it vacuous to check redundancy, or is it redundant to check vacuity?
Saved in:
| Title: | Is it vacuous to check redundancy, or is it redundant to check vacuity? |
|---|---|
| Authors: | Henkel, Elisabeth1 (AUTHOR) henkele@informatik.uni-freiburg.de, Hauff, Nico1 (AUTHOR) hauffn@informatik.uni-freiburg.de, Langenfeld, Vincent1 (AUTHOR) langenfv@informatik.uni-freiburg.de, Funk, Lena1 (AUTHOR) lenaf@tf.uni-freiburg.de, Podelski, Andreas1 (AUTHOR) podelski@informatik.uni-freiburg |
| Source: | Requirements Engineering. Jun2025, Vol. 30 Issue 2, p173-194. 22p. |
| Subjects: | Redundancy in engineering, Software requirements specifications, Mathematical logic, Formal languages |
| Abstract: | We present an automatic method to detect the existence of redundant requirements. A requirement is redundant if it does not represent an additional restriction on the intended behaviour of the specified system. If unintended, a redundancy may hint at a defect. The method applies to real-time requirements formalized in a particular kind of real-time logic formalism. The method uses techniques derived from real-time model checking. In particular, we use Phase Event Automata, a variant of timed automata. We introduce a novel determinism-preserving totalisation procedure for Phase Event Automata for the purpose of the automata-theoretic operation of complementation. The method is complete in the sense that it detects every redundancy in a given set of requirements. We have implemented the method. Preliminary experiments on industrial benchmarks indicate its scalability and its usefulness for discovering previously unknown defects. In spirit, redundancy is closely related to the property of vacuity. We show, however, that checking redundancy does not make checking vacuity redundant, and vice versa. This means that none of the two checks is superseeded by the other one. This article is the extension of a previous conference paper. [ABSTRACT FROM AUTHOR] |
| Copyright of Requirements Engineering is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
|
Full text is not displayed to guests.
Login for full access.
|
|
| Abstract: | We present an automatic method to detect the existence of redundant requirements. A requirement is redundant if it does not represent an additional restriction on the intended behaviour of the specified system. If unintended, a redundancy may hint at a defect. The method applies to real-time requirements formalized in a particular kind of real-time logic formalism. The method uses techniques derived from real-time model checking. In particular, we use Phase Event Automata, a variant of timed automata. We introduce a novel determinism-preserving totalisation procedure for Phase Event Automata for the purpose of the automata-theoretic operation of complementation. The method is complete in the sense that it detects every redundancy in a given set of requirements. We have implemented the method. Preliminary experiments on industrial benchmarks indicate its scalability and its usefulness for discovering previously unknown defects. In spirit, redundancy is closely related to the property of vacuity. We show, however, that checking redundancy does not make checking vacuity redundant, and vice versa. This means that none of the two checks is superseeded by the other one. This article is the extension of a previous conference paper. [ABSTRACT FROM AUTHOR] |
|---|---|
| ISSN: | 09473602 |
| DOI: | 10.1007/s00766-025-00438-5 |
