Conclusions

Abstract

The growth in software and hardware complexity demands more sophisticated system verification tools. For real-time systems, the critical property to be verified is that the system response time is within the specified bounds. While this task is relatively easy to do for the hardware part of the design, it is significantly harder for the software part. In this monograph we describe recent research done to attack this problem. We demonstrate that two distinct but related aspects make this a hard problem. The first of these, referred to as program path analysis, deals with handling the complexity of the potentially exponential number of program execution paths. It also attacks the hard problem of separating out the feasible execution paths from the infeasible ones. The second, referred to as microarchitecture modeling, deals with handling features of contemporary processors that make instruction execution times difficult to predict. We then highlight the need to consider the two problems together, pointing out the hard interdependence between them. Finally we present a unified analytical solution to this problem based on integer linear programming (ILP).