Information Technology Reference
In-Depth Information
Correct use of an abstraction is modelled as a state machine. The model
consists of a set of states and a set of possible transitions between the states.
State transitions are triggered by computation steps that are somehow related
to the modelled abstraction, e.g., the functions calls discussed in the socket
example above. These computation steps are called input symbols of the model.
In addition, models describe preconditions that must hold before input symbols
and how each of the input symbols affects the data flow.
At runtime, we track program's data flow to propagate the memory tags. In
addition, program's control flow is monitored in order to detect when the execu-
tion encounters an input symbol that should be passed to a state machine. The
correct state machine instance is determined by the data on which the computa-
tion step operates. A fault occurs if an input symbol is detected separately from
any state machine instance or if the corresponding state machine instance is in
a state for which there is no defined state transition for that particular symbol.
Typestate analysis and our approach have clear similarities, however our ap-
proach is in some ways more generic. Typestate analysis associates types with a
set of typestates that define allowed operations on each state. Each object of a
given type is in one of the related typestates in each program point. Those anal-
yses using residual runtime analysis must, similar to our approach, track object
instances. Instead of types, we focus on input symbols, some of which generate
tags, others of which change them. Between symbols, the data is considered sim-
ply as tagged memory areas. Even though a tagged memory area may equal to
an object of a certain type, we do not limit it to do so: a tag could equally well
represent objects of different types sharing some property.
Aliasing is not necessarily limited to copies of one abstraction, but instances
of different abstractions may also depend on each other. For example, the C
API offers two abstractions for file handling: low level file descriptors and higher
level buffered streams. An instance of one abstraction can be converted into an
instance of the other, and instances of both the abstractions sharing part of the
same state may be present simultaneously. Clearly, state transitions, e.g., clos-
ing a file, on one instance should be propagated to the others. However, sockets,
also represented as file descriptors, can too be converted into streams. Never-
theless, some socket operations are only available via the descriptor. Since not
every file used via the stream API is a socket, it makes sense to model protocols
for both the abstractions separately. To support modeling of dependencies be-
tween abstractions, we allow models to specify links that define effects of a state
transition in an instance of one abstraction to the other, related, instances.
3 Fault Detection Framework
In order to use the approach discussed so far, an abstraction must first be mod-
elled and the program must be instrumented to support data flow tracking. Then
the program is invoked with a test input and the execution path is automati-
cally checked for faults according to the modelled protocol. Finally, the results
are inspected by a tester.
