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 \to SA holds. However, none of such heuristics necessarily finds an "optimal implication".
After verifying SP \to SA, and the system implementing SP is deployed, performance changes as a result of powersaving, 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 \to 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 \to SA is still a theorem. Experimental results show that less than 20% overhead of the running time of the algorithm for the verification of SP \to SA is needed to find an optimal theorem.
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb