Scholarlink

<p>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.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Is it vacuous to check redundancy, or is it redundant to check vacuity?

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年6月3日

查看全文
  • Elisabeth Henkel,
  • Nico Hauff,
  • Vincent Langenfeld,
  • Lena Funk,
  • Andreas Podelski

摘要

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.