 |
 |
| |
|
|
Concurrent systems are systems composed of elements that can
operate concurrently and communicate with each other. Each component
can be viewed as a reactive system, i.e., a system that
continuously interacts with its environment. An example is a telephone
switching system, which performs many tasks concurrently and must
interact with subscribers, technicians, and other switches. The
software that controls a concurrent reactive system is notably hard
to design and test because its components may interact in many
unexpected ways. Traditional software testing techniques are of
limited help since test coverage is bound to be only a minute fraction
of the possible behaviors of the system. Furthermore, scenarios
leading to errors are often extremely difficult to reproduce. VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary code written in any language. The state space of a system is a directed graph that represents the combined behavior of all the components of the system. Paths in this graph correspond to sequences of operations (scenarios) that can be observed during executions of the system. VeriSoft systematically explores the state space of a system by controlling and observing the execution of all the components, and by reinitializing their executions. It searches for coordination problems (deadlocks, divergences, etc.) between concurrent components, and for violations of user-specified assertions. VeriSoft can always guarantee a complete coverage of the state space up to some depth; hence, all possible executions of the system up to that depth are guaranteed to be covered. Whenever an error is detected during state-space exploration, a scenario leading to the error state is saved in a file. Scenarios can be executed and replayed by the user with an interactive graphical simulator that can drive existing debuggers for examining the precise execution of the system processes. VeriSoft also supports a special operation to simulate nondeterminism. This operation can be used to easily model the environment of the system being analyzed. For instance, a single nondeterministic test script can conveniently specify a family of thousands of test scripts that will be automatically generated, executed and evaluated by VeriSoft. This nondeterministic operation can be used anywhere in the system (any language, any procedure, any process). VeriSoft has been applied successfully for analyzing (testing, debugging, reverse-engineering) several software products developed in Lucent Technologies, such as telephone-switching applications. Since VeriSoft can automatically generate, execute and evaluate thousands of tests per minute and has complete control over nondeterminism, it can quickly reveal behaviors that are virtually impossible to detect using conventional testing techniques.
|