Information Technology Reference
In-Depth Information
Fig. 5.
Behaviour of “close” function in extended text editor
There are however still aspects of the technique that do require expertise and
effort on the part of the developer. Currently, the QuickCheck template file (mi-
nus LTS) has to be generated by hand. This must include any relevant data state
information, along with appropriate data transformations. Furthermore, the de-
veloper has to manually identify a mapping from the low-level trace events to
abstract transition labels in the machine. Both can involve a substantial amount
of effort, which we aim to reduce in future work. This section will elaborate on
these problems, and will provide some preliminary suggestions for solutions.
5.1
Inferring Extended State Machines
The current approach, with the help of the EDSM algorithm, infers labelled
transition systems. In practice however, software behaviour cannot be completely
described by a simple LTS. In reality, the sequence of events or functions in a
program is also dependent upon the memory of the system; a particular function
may behave differently (and affect the state of the system in a different way)
depending on the state of the system when it is invoked.
To illustrate this problem, we envisage a slightly more sophisticated text editor
than the example in Figure 1. Imagine that, instead of only being able to open
one file at a time, the editor can open and edit multiple files concurrently. This
system can no longer be represented in a straightforward LTS with the same
labels we use in Figure 1. As a simple example, we focus in on the “close”
function. As illustrated in Figure 5, if multiple files are open, its behaviour
ultimately depends on how many files are open; if multiple files are open, it
is possible to close one of them and subsequently edit / save / close others.
However, if only one file is open, it is subsequently impossible to do any further
editing or saving. There are two different ways in which “close” can affect the
subsequent behaviour of the software system, and this depends on the underlying
state of the system. This more complex, data state-dependent behaviour cannot
be represented on a simple deterministic LTS.
There are two approaches that attempt to address this problem. The first
approach, which is currently adopted by the authors, is to ensure that functions
are chosen in such a way that the different data constraints are encompassed
