OPTIMIZING TIMING ANALYSIS AND VERIFICATION OF EMBEDDED SYSTEMS USING RULE-BASED-ANALYTIC TECHNIQUES

In previous work we have developed very fast static techniques to determine response times of rule-based programs. This paper shows that the problem of formal verification of embedded systems can be represented as the problem of determining response time of rule-based systems. We do this by encoding the specification and safety assertion given in RTL as a rule-based EQL or MRL program. This paper goes on to show that our approach requires quadratic time while the equivalent RTL approach requires exponential time in the worst case.