Information Technology Reference
In-Depth Information
also uncovered a few remaining errors in the Wring tool. The resulting automata
generated by our tool and LTL2Buchi are very similar in size, perhaps not very
surprising since similar translation algorithms are used. However, on average our
implementation generates about 1% smaller automata, when tested on randomly
generated LTL formulas.
The development process (the implementation was carried out using property
driven development supported by the QuickCheck tool) for the LTL-to-Buchi
translator, as well as the implementation and the result of the evaluation are
described in [EF09].
7ToolIn g on
In addition to work on the individual tools and methods described above, we
aim to integrate the tools we are building in a number of ways. As a first step,
we focused on the verification of the global process registry with an approach
that combined QuickCheck and McErlang. Here, the QuickCheck tool was used
to generate a number of test sequences for the global process registry; these
were then fed to McErlang which explored all possible interleavings of the test
sequences using its model checking algorithms. Finally the results (a set of se-
quences of return values of a set of API calls) were checked using the QuickCheck
tool. Early results are promising, as the combined tool set was also able to
discover race conditions in the global process registry.
We are also working on a integration of the other relevant tools. Essentially
we want to be able to run a set of QuickCheck tests where the program under
test is capable of being controlled by different schedulers: (i) either using the
standard Erlang program scheduler, or (ii) using the PULSE scheduler which
offers more control over scheduling and a more random behaviour, or (iii) the
program is controlled by the McErlang model checker which in theory can fully
explore the state space corresponding to any given test case.
As an example of how the tools and methodologies can be integrated consider
the following example, where we describe how we can refactor a test suite into
properties.
7.1
Example
The test suite in this example is 2228 lines of code, containing 4 groups of test
cases:
-
5 test cases in the create group,
-
4 test cases in the set topology group,
-
11 test cases in the modify group,
-
10 test cases in the delete group.
It is clear that certain test cases have some similarity. For example, we have a
number of occurrences where a test case for audio is repeated for video. There
are two ways in which we can work with this in the refactoring tool: We can
