Doron A. Peled
Path Exploration Tool: A Tool for Interactive Software Testing
We describe here the PET (standing for path exploration tool)
system, developed in Bell Labs. This new tool allows an
interactive testing of sequential or concurrent programs,
using techniques taken from deductive program verification.
It automatically generates and displays a graphical representation
of the flow graph, and links the visual representation
to the code. Testing is done by selecting execution paths,
or, in the case of concurrent programs, interleaved sequences
of code. The PET system calculates the exact condition
to execute path being selected, in terms of the program variables.
It also calculates (when possible) whether this condition
is vacuous (never satisfied) or universal (always satisfied).
The user can then edit the path and select variants of it by
either extending it, truncating it, or switching the order of
appearance of concurrent events. This testing approach is not
limited to finite state systems, and hence can be used in cases
where a completely automatic verification cannot be applied.