Incremental methods for checking real-time consistency

TL;DR

This paper introduces incremental algorithms for verifying real-time consistency in requirements using discrete-time timed automata, improving the efficiency of detecting conflicts and errors in requirements specifications.

Contribution

It generalizes and formalizes notions of rt-consistency and partial consistency, and develops three novel incremental algorithms with experimental validation.

Findings

Algorithms effectively detect inconsistencies in requirements.

Incremental methods outperform non-incremental approaches.

Experimental results demonstrate practical applicability.

Abstract

Requirements engineering is a key phase in the development process. Ensuring that requirements are consistent is essential so that they do not conflict and admit implementations. We consider the formal verification of rt-consistency, which imposes that the inevitability of definitive errors of a requirement should be anticipated, and that of partial consistency, which was recently introduced as a more effective check. We generalize and formalize both notions for discrete-time timed automata, develop three incremental algorithms, and present experimental results.