rt-inconsistency: A new property for real-time requirements

Abstract

We introduce rt-inconsistency, a property of real-time requirements. The property reflects that the requirements specify apparently inconsistent timing constraints. We present an algorithm to check rt-inconsistency automatically. The algorithm works via a stepwise reduction to real-time model checking. We implement the algorithm using an existing module for the reduction and the Uppaal tool for the real-time model checking. As a case study, we apply our prototype implementation to existing real-time requirements for automotive projects at Bosch. The case study demonstrates the relevance of rt-inconsistency for detecting errors in industrial real-time requirements specifications. © 2011 Springer-Verlag.