Data Parallel Program Visualizations from Formal Specifications

As software is used increasingly to control critical systems, program correctness becomes paramount. Correctness is particularly important for parallel and distributed programs since the effects of a single programming error may be magnified greatly due to the parallelism. Using formal specification languages to describe programs minimizes the number of errors that would have been introduced using informal approaches to software development. This paper describes a project that combines formal specifications and visualizations to assist in testing and debugging a parallel program. The Lockheed Integrated Visualization Environment (LIVE) system is a graphical rule-based environment that aids a programmer in the creation of visualizations that depict the behavior of executing programs. The choice of visualization corresponds to the type of programs visualized and the type of errors expected. In order to facilitate the decision-making process, LIVE uses the formal specifications of the program′s data structures to guide the visualization generation process.