The GIST Behavior Explainer

One difficulty in understanding formal specifications is that there are often interactions between pieces of the specification, never explicitly stated, that only become apparent when the specification is analyzed or simulated. Symbolic evaluation has been proposed as a way of making such interactions apparent, but symbolic evaluators often produce enormous execution traces that are tedious and difficult to examine. This paper presents an automated system that employs a number of heuristics to select the most interesting aspects of the trace for presentation. The system uses this information to construct an English description of the trace. Due to the need for summarization and proof reformulation, the direct-translation approach, which worked well in describing specifications statically, is not suitable in this case. This paper describes the system and gives an example of its output.

Authors

• Bill Swartout

Keywords

No keywords are indexed for this paper.