Scenario-based timing verification of multiprocessor embedded applications

Abstract

This work presents a static timing-analysis method for verification of scenario-based real-time properties, on graphical task-level models of embedded applications. Scenario-based properties specify timing constraints which must be honored for specific control-flow behaviors and task execution orderings. Static checking of scenario-based properties currently requires computationally expensive model checking methods. Hence the proposed graph-based static timing-analysis algorithm improves upon the state-of-the-art. This is manifested in a significant performance advantage over timed model checking (up to 1000X in several cases), which suffers from state space explosion. The proposed algorithm also employs compositional reasoning and abstraction refinement for handling large problems. We also illustrate methods for using scenario-based timing analysis, which can act as alternatives to traditional timed model checking for verification of timed systems like FDDI and Fischer protocols. We implement this timing verification algorithm as a tool called SymTime and present experimental results for SymTime comparing it with SPIN, UPPAAL, and a TCTL model checker for Time Petri Nets, called Romeo.