Doron A. Peled
University of Texas at Austin, USA
Tracing the executions of concurrent programs
Concurrent programs are highly prone to errors, while
analyzing and debugging them is known to be a very difficult task.
Applying automatic and manual verification and validation techniques
to such programs is a nontrivial challenge. We describe
here two techniques, which help the user to interactively
analyze and debug concurrent programs.
The first method is the symbolic execution of traces of the
program. We compile a visual representation, in the form of a
flow graph of the concurrent processes, with one window for each
concurrent process. The user is allowed to select an interleaved
execution path. The system automatically calculates the weakest
condition for executing the path, and tries to simplify it
as much as possible. Such a path is not limited to start from
the beginning of the program, nor do the variables need to
be fully initialized. By selecting such paths, obtaining
the conditions to execute them, and interactively changing them
(e.g., by changing the order of interleaving concurrent actions, or
providing a different suffix), we can obtain a better
understanding of the program, and perform some simple verification
tasks. This technique is implemented by the PET tool.
Another method employed by this tool is based on the
application of temporal logic, as a way of assisting the debugging
of a concurrent or a sequential program. Temporal logic
over finite sequences is used here as a constraint formalism
that is used to control the way we step through the states of
the debugged system. Using such temporal specification and various
search strategies, we are able to traverse the executions of
the system and obtain important intuitive information
about its behaviors.
In this talk the tool and techniques will
be described and demonstrated.
Doron has all his degrees from the Technion, Israel Institute of
Technology. Graduating his DSc in 1991, he has spent a postdoc year at the
University of Warwick, UK. Doron is working in the area of formal methods,
and is interested in deductive verification, model checking and testing, as
well as combining these methods, and developing methodologies to improve the
reliability of software. He is a coauthor of the book "model checking" and
the author of the recent book "software reliability methods". Doron has
worked in Bell Laboratories from 1992 to 2001 as a member of technical
staff, and then moved to the University of Texas at Austin. Starting
September 2002, Doron is joining again the University of Warwick as a
professor of software engineering in the department of Computer Science.