Document Type

Technical Report

Department

Computer Science and Engineering

Publication Date

1994-01-01

Filename

WUCS-94-8.PDF

Technical Report Number

WUCS-94-8

Abstract

Formal methods hold the promise for high dependability in the design of critical software. However, software engineers who employ formal methods need to communicate their design decisions to users, customers, managers, and collegues who may not be in a position to acquire a full understanding of the formal notation being used. Visualizations derived from formal specifications and designs must be able to convey the required information precisely and reliably without the use of formal notation. This paper discusses a design methodology which attempts to integrate a design methodology based upon specification and program refinement with a state-of-the-art approach to rapid visualization of executing programs. The emphasis is placed on how to convey graphically various kinds of formally-stated program properties. The illustrations are extracted from a case study involving the formal derivation of a message router. The ultimate goal is to identify issues fundamental to the use of visualization in conjunction with formal methods and to catalog techniques which achieve effective visual communication withou compromising formal reasoning.

Comments

Permanent URL: http://dx.doi.org/10.7936/K70Z71J4

Download

Share

COinS