Combining static and dynamic analysis of concurrent programs

Concurrent systems are inherently more difficult to analyze and visualize than sequential programs. The difficulty of producing correct concurrent programs is mirrored in maintenance as difficulty in extracting a correct high-level model of task interactions and predicting the effect of a modification to portions of a system. We advocate a methodology that combines static analysis of an abstract model with dynamic analysis of source code. While the abstract model is is amenable to exhaustive analysis, dynamic analysis is capable checking richer classes of specifications, and moreover provides a check on the correctness of simplifications and assumptions inherent in abstract models. We illustrate this approach by combining two tools, the PAL system for compositional reachability analyses and the FORESEE analysis tool for temporal analysis of runtime traces, applied to a simulation scenario