Databases Reference
In-Depth Information
8.3
Inference Experiments :::::::::::::::::::::::::::::::::::::::::::::::::::: 268
8.3.1
Daisy :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 271
8.3.1.1
Inference Results ::::::::::::::::::::::::::::::::::::::::: 272
8.3.2
JBoss Application Server :::::::::::::::::::::::::::::::::::::::::: 273
8.3.2.1
Inference Results ::::::::::::::::::::::::::::::::::::::::: 273
8.3.2.2
Comparison with JTA Specication ::::::::::::::::::::: 274
8.3.3
Windows ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 277
8.3.3.1
Inference Results ::::::::::::::::::::::::::::::::::::::::: 277
8.4
Using Inferred Properties ::::::::::::::::::::::::::::::::::::::::::::::::: 280
8.4.1
Program Verication :::::::::::::::::::::::::::::::::::::::::::::: 280
8.4.1.1
Daisy ::::::::::::::::::::::::::::::::::::::::::::::::::::: 281
8.4.1.2
Windows ::::::::::::::::::::::::::::::::::::::::::::::::: 283
8.4.2
Program Dierencing ::::::::::::::::::::::::::::::::::::::::::::: 285
8.4.2.1
Tour Bus Simulator :::::::::::::::::::::::::::::::::::::: 286
8.4.2.2
OpenSSL ::::::::::::::::::::::::::::::::::::::::::::::::: 288
8.5
Related Work ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 294
8.5.1
Grammar Inference :::::::::::::::::::::::::::::::::::::::::::::::: 294
8.5.2
Property Inference :::::::::::::::::::::::::::::::::::::::::::::::: 294
8.5.2.1
Template-Based Inference ::::::::::::::::::::::::::::::: 295
8.5.2.2
Arbitrary Model Inference ::::::::::::::::::::::::::::::: 296
8.5.3
Use of Inferred Specications ::::::::::::::::::::::::::::::::::::: 297
8.5.3.1
Defect Detection ::::::::::::::::::::::::::::::::::::::::: 297
8.5.3.2
Other Uses ::::::::::::::::::::::::::::::::::::::::::::::: 298
8.6
Conclusion ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 299
Acknowledgments ::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 301
Bibliography ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 301
8.1 Introduction
For many years, researchers have claimed that software specifications can
be used to improve many software development activities. A formal specifi-
cation documents important properties and hence is useful in understanding
programs [41,67]. Formal specifications can be used to automatically generate
test inputs [14, 21, 60]. Program verification needs a formal specification that
defines the correct behaviors of a program [34, 41, 67]. Other uses include re-
fining a specification into a correct program [1] and protecting a programmer
from making changes that violate important invariants [26].
Despite these benefits, formal specifications are rarely available for real
systems [42, 52, 54]. To help realize the benefits of formal specifications, this
work develops techniques for automatically inferring formal specifications and
investigates the uses of inferred specifications in software development.
Search WWH ::
Custom Search