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.
|
|
| FullText | Links: – Type: pdflink Text: Availability: 1 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 187141986 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Is it vacuous to check redundancy, or is it redundant to check vacuity? – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Henkel%2C+Elisabeth%22">Henkel, Elisabeth</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> henkele@informatik.uni-freiburg.de</i><br /><searchLink fieldCode="AR" term="%22Hauff%2C+Nico%22">Hauff, Nico</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> hauffn@informatik.uni-freiburg.de</i><br /><searchLink fieldCode="AR" term="%22Langenfeld%2C+Vincent%22">Langenfeld, Vincent</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> langenfv@informatik.uni-freiburg.de</i><br /><searchLink fieldCode="AR" term="%22Funk%2C+Lena%22">Funk, Lena</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> lenaf@tf.uni-freiburg.de</i><br /><searchLink fieldCode="AR" term="%22Podelski%2C+Andreas%22">Podelski, Andreas</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> podelski@informatik.uni-freiburg</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Requirements+Engineering%22">Requirements Engineering</searchLink>. Jun2025, Vol. 30 Issue 2, p173-194. 22p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Redundancy+in+engineering%22">Redundancy in engineering</searchLink><br /><searchLink fieldCode="DE" term="%22Software+requirements+specifications%22">Software requirements specifications</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+logic%22">Mathematical logic</searchLink><br /><searchLink fieldCode="DE" term="%22Formal+languages%22">Formal languages</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=187141986 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s00766-025-00438-5 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 22 StartPage: 173 Subjects: – SubjectFull: Redundancy in engineering Type: general – SubjectFull: Software requirements specifications Type: general – SubjectFull: Mathematical logic Type: general – SubjectFull: Formal languages Type: general Titles: – TitleFull: Is it vacuous to check redundancy, or is it redundant to check vacuity? Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Henkel, Elisabeth – PersonEntity: Name: NameFull: Hauff, Nico – PersonEntity: Name: NameFull: Langenfeld, Vincent – PersonEntity: Name: NameFull: Funk, Lena – PersonEntity: Name: NameFull: Podelski, Andreas IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 06 Text: Jun2025 Type: published Y: 2025 Identifiers: – Type: issn-print Value: 09473602 Numbering: – Type: volume Value: 30 – Type: issue Value: 2 Titles: – TitleFull: Requirements Engineering Type: main |
| ResultId | 1 |
