Automated Symbolic Timing Analysis for Distributed Systems
A timing property of a distributed system is an assertion about
the time intervals between events in executions of that system. There
are three traditional approaches to determining timing properties of
distributed systems: measurement, simulation, and analysis. Results
from analysis can be symbolic and therefore much more general than
results from measurement and simulation. For example, analysis can
express the end-to-end delay of an atomic commitment protocol
symbolically as a function of message delay and other system parameters.
However, manual analysis of distributed algorithms is often tedious and
error-prone. We have developed and implemented a
state-exploration-based analysis that can automatically determine a
large class of timing properties of distributed systems.
Scott Stoller's Home Page