Scalable Analysis of Real-Time Requirements

Detecting issues in real-time requirements is usually a trade-off between flexibility and cost: the effort expended depends on how expensive it is to fix a defect introduced by faulty, ambiguous or incomplete requirements. The most rigorous techniques for real-time requirement analysis depend on the formalisation of these requirements. Completely formalised real-time requirements allow the detection of issues that are hard to find through other means, like real-time inconsistency (i.e., "do the requirements lead to deadlocks and starvation of the system?") or vacuity (i.e., "are some requirements trivially satisfied"). Current analysis techniques for real-time requirements suffer from scalability issues – larger sets of such requirements are usually intractable. We present a new technique to analyse formalised real-time requirements for various properties. Our technique leverages recent advances in software model checking and automatic theorem proving by converting the analysis problem for real-time requirements to a program analysis task. We also report preliminary results from an ongoing, large scale application of our technique in the automotive domain at Bosch.