 |
 |
| |
|
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.
Concurrent reactive systems are notably hard to design because their components may interact in many unexpected ways. Traditional testing techniques are of limited help since test coverage is bound to be only a minute fraction of the possible behaviors of the system. Moreover, bugs in concurrent systems are usually very hard to reproduce and hence hard to understand.
VeriSoft can help detecting and reproducing most of these expensive and subtle coordination problems:
Systematic State-space exploration (also often referred to as "model checking") is one of the most successful strategies for analyzing the correctness of models of concurrent reactive software systems. It consists of exploring a directed graph, called the state space, representing the combined behavior of all concurrent components in the system. Previously existing state-space exploration tools are restricted to the analysis of a model (simplified description) of a concurrent reactive software system. Typically, such a model is specified manually in a modeling language (usually some kind of extended finite-state machine notation).
The technical contribution of VeriSoft is to extend the scope of systematic state-space exploration from modeling languages to programming languages. For instance, VeriSoft can analyze concurrent systems composed of several concurrent processes executing arbitrary code. This is possible thanks to the use of new efficient state-space search techniques (see [Documentation]).
By extending the scope of systematic state-space exploration from modeling languages to general-purpose programming languages, VeriSoft eliminates one major obstacle to a wider use of this paradigm, namely the need to build a model of the application to be analyzed. The elimination of this time-consuming and error-prone task (plus the non-negligible effort needed to become familiar with a modeling language) makes systematic state-space exploration much more attractive and economically feasible for applications developed in an industrial environment, where systems are always developed under time pressure.
VeriSoft is WYSIWYG! (What You See/Simulate Is What You Get)
VeriSoft systematically searches the state space of a concurrent reactive software system by generating, controlling, and observing the possible executions and interactions of all its components. It integrates automatic test generation, execution and evaluation in a single framework.
Four basic types of errors can be searched for by VeriSoft:
When an error is detected, the state-space exploration is stopped, and a scenario leading to the error is generated. This scenario can then be replayed and examined with the VeriSoft simulator.
VeriSoft analyzes closed systems: the environment of one process/component is formed by the other processes/components of the system. This implies that, in the case of an ``open'' system interacting with its environment, the environment in which the open system operates has to be represented, possibly using other processes, and is part of the system being analyzed by VeriSoft.
In practice, a complete representation of such an environment may not be available, or may be very complex. It is then convenient to use a simplified representation (software stub) to simulate the behavior of the environment visible to the application under test. Another reason for providing a specific representation of the environment is to test the system under specific external constraints (test driver).
For this purpose, VeriSoft supports a special operation ``VS_toss'' to express a valuable feature of modeling languages, not found in programming languages: nondeterminism.
The operation VS_toss takes as argument a positive integer n, and returns an integer in [0,n]. This operation can be executed by any process and is nondeterministic: the execution of VS_toss(n) may yield up to n+1 different successor states in the state space of the system, each of which corresponds to a different value returned by VS_toss.
Nondeterminism can be used to easily model the environment of an open system. 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. The nondeterministic operation VS_toss can be used anywhere in the system (any language, any procedure, any process).