Optimization of Real-Time Systems Timing Specifications

Real-time logic (RTL) is useful for the verification of a safety assertion SA with respect to the specification SP of a real-time system. Since the satisfiability problem for RTL is undecidable, there were many efforts to find proper heuristics for proving that SPrarrSA holds. However, none of such heuristics necessarily finds an "optimal implication". After verifying SPrarrSA, and the system implementing SP is deployed, performance changes as a result of power-saving, faulty components, and cost-saving in the processing platform for the tasks specified in SP affect the computation times of the specified tasks. This leads to a different but related SP, which would violate the original SPrarrSA theorem if SA remains the same. It is desirable, therefore, to determine an optimal SP with the slowest possible computation times for its tasks such that the SA is still guaranteed. This is clearly a fundamental issue in the design and implementation of highly dependable real-time/embedded systems. This paper tackles this fundamental issue by describing a new method for relaxing SP and tightening SA such that SPrarrSA is still a theorem. Experimental results show that less than 20% overhead of the running time of the algorithm for the verification of SPrarrSA is needed to find an optimal theorem