A Practical and Complete Method for Detecting rt-Inconsistencies in Real-Time Requirements
摘要
[Context and motivation] Methods to automatically detect an rt-inconsistency, a notorious defect in real-time requirements, have proven to be practically useful. Existing methods scale to industrial examples. They are, however, not complete, meaning that they cannot detect every rt-inconsistency. [Question/problem] The question is whether one can achieve both scalability and completeness. [Principal ideas/results] We adapt an existing (incomplete) method so that it takes, as a configurable parameter, a set of candidate subsets of requirements. We develop an algorithm that selects such a set, guaranteed to be large enough to ensure completeness, yet potentially small enough to ensure scalability. Our experimental evaluation demonstrates that the resulting complete method indeed scales to industrial examples. It can detect previously unknown defects and, rather than incurring an overhead, can even be more efficient. [Contribution] We present—to the best of our knowledge—the first method for detecting rt-inconsistencies that is both practical and complete. We prove its completeness and present an experimental evaluation.