Information Technology Reference
In-Depth Information
Input
:
Prog
,
Σ
Pos←∅
;
Neg←∅
;
1
LT S ← generateInitLTS
(
Σ
);
2
Test← generateTests
(
LT S
);
3
foreach
test ∈ Test
do
4
(
trace, pass
)
← runT est
(
test, P rog
);
5
if
pass
then
6
Pos← Pos∪{trace}
;
7
trace ∈ L
LTS
then
if
8
LT S ← EDSM
(
Pos,Neg
);
9
Test← generateTests
(
LT S
);
10
11
else
12
Neg ← Neg∪{trace}
;
13
trace ∈ L
LTS
then
if
14
LT S ← EDSM
(
Pos,Neg
);
15
Test← generateTests
(
LT S
);
16
17
end
18
end
19
return
LT S
20
Algorithm 2.
InferWithTests
contain data transformations that manipulate some underlying memory. As it
stands, the inference algorithm is restricted to inferring the LTS, and extending
it to deal with data-constraints will be discussed in section 5. In its current form,
these elements are supplied by the user in the form of a template. The data-state,
along with the way elements in
Σ
change it, is specified by the user and made
available as a template file.
The EDSM algorithm has been implemented by the authors in their Stat-
eChum tool [12,21]. Traces are recorded by using the comprehensive tracing
framework that is built into the Erlang OTP [2]. Given the template file gen-
erated by the user, a simple Bash script is used to orchestrate the interac-
tion between the QuickCheck testing/tracing process and the StateChum model
inference framework.
4 Case Study - Reverse-Engineering a TCP Stack
The ProTest project has involved a selection of case studies, to explore the
ecacy of the various tools and techniques that are being developed. One of
those case studies is a comprehensive QuickCheck testing specification for TCP
stacks, which was developed by Paris and Arts [22]. To provide a preliminary
assessment of our technique, we have applied it to this case-study, with the aim
of reverse-engineering an accurate model of a Linux TCP/IP implementation
(via a TCP testing extension of the QuickCheck framework).
