Databases Reference
In-Depth Information
to diagnose. Furthermore, many of the inferred properties are not properly
documented. In our personal communication with several Windows develop-
ers, they expressed the need for a tool to help them learn the important rules
of Windows such as the ones Perracotta infers. For example, two summer in-
terns in the Windows group were assigned a task of writing a program using
a type of queue in Windows kernel. Unfortunately they could not find any
documentation about this queue. As a result, they had to manually look at
programs to distill the rules about how to use the queue, which was very
time-consuming.
8.4 Using Inferred Properties
This section presents experiments using the inferred properties. Section
8.4.1 describes experiments using a verification tool to check the inferred
properties. Section 8.4.2 describes experiments using the inferred properties
to identify differences among multiple versions of a program.
8.4.1 Program Verification
Program verification techniques try to decide whether or not a program
conforms to a specification. Although verifying any non-trivial property is
undecidable [72], recently researchers have achieved much practical success in
verifying important generic safety properties [9] as well as application-specific
properties [5, 19, 27, 78]. For example, Microsoft uses the Static Driver Verifier
(also known as the SLAM project) to check device drivers against a list of
driver-related rules. The adoption of such tools, however, is limited by the
unavailability of property specifications.
Satisfaction or
Counter-
examples
Inferred
Properties
Program
FIGURE 8.21: Use inferred properties in program verification.
We present two case studies on the Daisy file system and the Microsoft
Windows kernel respectively. Figure 8.21 illustrates this process. In particular,
we used the ESP verifier to check the Windows kernel, properties and the Java
PathFinder model checker to verify the Daisy properties [19, 78].
Search WWH ::
Custom Search