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 SP -> SA holds. However,
none of such heuristics necessarily finds an "optimal implication".
After verifying SP -> SA, 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 SP -> SA 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 SP -> SA is still a theorem.
Experimental results show that only about 10% of the running time of the
heuristic for the verification of SP -> SA is needed to find an optimal
theorem.