Dynamic Analysis for Self-Healing
Software
Mauro Pezzè
Università degli Studi di Milano Bicocca
University of Lugano
PART I: Dynamic Analysis
Program verification
Testing
(sampling)
Analysis
(folding)
Dynamic
Static
(execution traces) (execution space)
Dynamic analysis
Ernst: Daikon…..
Dynamic memory analysis -> purify
Lamport: dynamic race detection ->lockset analysis
performance analysis
debugging
1960
1970
1980
1978
1990
1989
2000
1999
Dynamic lockset analysis
Tread
thread A
Program trace
lock(lck1)
x=x+1
unlock(lck1)
thread B
lock(lck2)
x=x+1
unlock(lck2)
locks held
lockset(x)
{}
{lck1, lck2}
{lck1}
{lck1}
{}
{lck2}
{}
{}
Lockset analysis
Virgin
write
read/write/first thread
Exclusive
read/new thread
write/new thread
Shared-Modified
read
Shared
write
Dynamic memory analysis
allocate
Unallocated
(unwritable and unreadable)
deallocate
Allocated and uninitialized
(writable, but unreadable)
deallocate
initialize
Allocated and initialized
(readable and writable)
Possible invariants
x=a
x = uninit
x = {a,b,c}
….
Program
execution
Actual invariants
x={ , }
y>x
….
Daikon
POSSIBLE INVARIANTS
over any variable x:
x=a
x = uninit
x = {a,b,c} for a small set of values
over a single numeric variable x:
x >= a, x <= b, a <= x <= b
x¬=0
x = a (mod b)
x ¬ = a (mod b)
over two numeric variables x and y:
y = ax+b
x <= y, x < y, x = y, x ¬ = y
x = f n(y)
over the sum of two numeric variables x+y:
x+y >= a, x+y <= b, a <= x+y <= b
x+y ¬ = 0
x+y = a (mod b)
x+y ¬ = a (mod b)
…………
Dynamic analysis of COTS components
From simple variables to complex objects
Extract information with aspect programming
Identify field values with reflection
Derive invariant on objects’ fields (Daikon)
client
refs
cart
cartitem.getUnitCost <= cartitem.getTotal
Dynamic analysis of subsystems’ interactions
single interactions == words over a regular
language
getitem getitem getpicture
getitem getitem getitme getpicture
interaction models == FSA
Deriving Interaction Models
• From samples to FSA
–
–
–
–
–
only positive samples
shared sub-behaviors
no teacher
incremental algorithm
add-and-delete sequence
kBehavior
b
a
abbfdedec
abbfdedec
f
c
c
e
d
f
From FSA to extended FSA:
a simple set of traces
createBoard
[type= ]
[choice= ]
createAMD
[type= ]
[choice= ]
createRAM
]
[mb=
[choice= ]
createHD
[type= ]
[choice= ]
createVideo
[type= ]
[choice= ]
createAudio
[type= ]
[choice= ]
createModem
[type= ]
[choice= ]
createBoard
[type= ]
[choice= ]
createAMD
[type= ]
[choice= ]
createRAM
]
[mb=
[choice= ]
createHD
[type= ]
[choice= ]
createVideo
[type= ]
[choice= ]
createAudio
[type= ]
[choice= ]
createLAN
[type= ]
[choice= ]
createBoard
[type= ]
[choice= ]
createIntel
[type= ]
[choice= ]
createRAM
]
[mb=
[choice= ]
createHD
[type= ]
[choice= ]
createVideo
[type= ]
[choice= ]
createAudio
[type= ]
[choice= ]
createLAN
[type= ]
[choice= ]
createBoard
[type= ]
[choice= ]
createAMD
[type= ]
[choice= ]
createAMD
[type= ]
[choice= ]
createRAM
]
[mb=
[choice= ]
createHD
[type= ]
[choice= ]
[type=choice]
createVideo
[type= ]
[choice= ]
createLAN
[type= ]
[choice= ]
A simple FSA
createAMD
createBoard
createHD
createRAM
createAudio
createModem
createVideo
crateAMD
createIntel
createRAM
createVideo
createLAN
createAudio
createHD
createVideo
createLAN
An annotated FSA
createBoard
createAMD
createRAM
createHD
createVideo
createAudio
createModem
[type= ]
[choice= ]
[type= ]
[choice= ]
[type=
]
[choice= ]
[type= ]
[choice= ]
[type= ]
[choice= ]
[type= ]
[choice= ]
[type= ]
[choice= ]
createVideo
createAudio
createLAN
[type= ]
[choice= ]
[type= ]
[choice= ]
[type= ]
[choice= ]
createRAM
[type=
]
[choice= ]
createBoard
createHD
[type= ]
[choice= ]
[type= ]
[choice= ]
createAudio
createRAM
createIntel
[type= ]
[choice= ]
[type=
]
[choice= ]
createVideo
createHD
[type= ]
[choice= ]
[type= ]
[choice= ]
[type= ]
[choice= ]
createLAN
[type= ]
[choice= ]
createBoard
[type= ]
[choice= ]
createAMD
[type= ]
[choice= ]
createAMD
createRAM
createHD
[type= ]
[choice= ]
[type=
]
[choice= ]
[type= ]
[choice= ]
[type=c]
createVideo
createLAN
[type= ]
[choice= ]
[type= ]
[choice= ]
Precision: the simple FSA
createAMD
createBoard
createHD
createRAM
createAudio
createModem
createVideo
crateAMD
createIntel
createRAM
createVideo
createLAN
createAudio
createHD
createVideo
createLAN
Precision: the annotated FSA
createBoard
[type= ]
[choice= ]
createAMD
createRAM
createHD
createVideo
createAudio
createModem
[type= ]
[choice= ]
[type=
]
[choice= ]
[type= ]
[choice= ]
[type= ]
[choice= ]
[type= ]
[choice= ]
[type= ]
[choice= ]
createVideo
createAudio
createLAN
[type= ]
[choice= ]
[type= ]
[choice= ]
[type= ]
[choice= ]
createRAM
[type=
]
[choice= ]
createBoard
createHD
[type= ]
[choice= ]
[type= ]
[choice= ]
createAudio
createRAM
createIntel
[type= ]
[choice= ]
[type=
]
[choice= ]
createVideo
createHD
[type= ]
[choice= ]
[type= ]
[choice= ]
[type= ]
[choice= ]
createLAN
[type= ]
[choice= ]
createBoard
[type= ]
[choice= ]
createAMD
[type= ]
[choice= ]
createAMD
createRAM
createHD
[type= ]
[choice= ]
[type=
]
[choice= ]
[type= ]
[choice= ]
[type=c]
createVideo
createLAN
[type= ]
[choice= ]
[type= ]
[choice= ]
PART II: Self-Healing Software
The self-healing cycle
Detect
(predict)
failures
Verify
the new
system
Diagnose
faults
Heal
faults
Detect (predict) failures
Expected
system
behavior
Detect
(predict)
failures
compare
Actual
system
behavior
We need a model
of the system
expected behavior
Diagnose faults
Correct
Execution
Trace
diagnose
faults
compare
Actual
Execution
Trace
Specification
of execution
properties
Model of
dynamic
behavior
heal faults
heal
faults
fault
Fault taxonomy
Healing
strategies
Dynamic models to diagnose faults
1.- Collect dynamic
information
legal behaviors
component
“stable”
system
b
In a
“stable
environment”
a
f
c
c
e
d
f
Dynamic models to diagnose faults
component
2.- Collect behavior
information in a
experienced behaviors
New
system 2
new environment
c
f
b
a
e
c
d
f
3.- Compare to identify
potential faults
failure information
legal behaviors
Fault localization
b
a
f
c
c
e
d
f
Sun’s Pet store
generate information for fault diagnosis
legal behaviors
GUI
Customer
handler
test
cases
Pet Store v1
b
a
f
c
c
e
d
f
Detect
(predict)
failures
Verify
the new
system
Pet Store
Diagnose
faults
Failure condition:
Required(e-mail address)
Heal
faults
Detect
failures
No e-mail address
inputs
experienced behaviors
b
a
f
c
c
e
d
f
Record
behaviors
New GUI
Modified
Customer
handler
Pet Store v2
Detect
(predict)
failures
Verify
the new
system
Pet Store
Diagnose
faults
legal behaviors
Heal
faults
New GUI
Modified
Customer
handler
failure
c
f
b
a
e
c
d
f
differences
experienced behaviors
Pet Store v2
b
a
f
c
c
e
d
f
CustomerEvent.getContactInfo.getEmail.length>5
Pet Store: fault localization
CustomerEvent.getContactInfo.getEmail.length>5
The value of field length
is not checked for
Non emptiness
Computer store
generate information for fault diagnosis
legal behaviors
Catalog
handler
b
a
test
cases
Computer store
v1
f
c
c
e
d
f
Detect
(predict)
failures
Verify
the new
system
Computer Store
Diagnose
faults
Failure condition:
Return (complete catalog)
Heal
faults
Detect
failures
Incomplete catalog
inputs
New Catalog
handler
experienced behaviors
b
a
f
c
c
e
d
f
Record Computer store
behaviors
v2
Detect
(predict)
failures
Verify
the new
system
Computer Store
Diagnose
faults
legal behaviors
Heal
faults
New Catalog
handler
failure
c
f
b
a
e
c
d
f
differences
Computer store
v2
experienced behaviors
b
a
getCatalog: S|(SCC*R)
f
c
c
e
d
f
S = locate service
C = extract catalog
R= produce results
Computer Store: fault localization
getCatalog: S|(SCC*R)
The new catalog
Generate SS*sequences
==
Arbitrary nesting of categories
incompatible with the DB
S = locate service
C = extract catalog
R= produce results
Hermes mobile middleware
generate information for fault diagnosis
legal behaviors
logger
b
a
test
cases
Hermes v2.02
f
c
c
e
d
f
Detect
(predict)
failures
Verify
the new
system
Hermes
Diagnose
faults
Failure condition:
Close all threads
Heal
faults
Detect
failures
Open threads
inputs
New logger
experienced behaviors
b
a
f
c
c
e
d
f
Record
behaviors
Hermes 2.05
Detect
(predict)
failures
Verify
the new
system
Hermes
Diagnose
faults
legal behaviors
Heal
faults
failure
c
f
b
e
New logger
a
c
d
f
differences
experienced behaviors
Hermes 2.05
b
a
“dangling thread”
f
c
c
e
d
f
Hermes: fault localization
“Dangling threads”
Kill dangling threads before quitting
Jedit
generate information for fault diagnosis
legal behaviors
Jdiff Plugin
1.3.2
b
a
test
cases
Jedit 4.1
f
c
c
e
d
f
Detect
(predict)
failures
Verify
the new
system
Jedit
Diagnose
faults
Failure condition:
Display all GUI elements
Heal
faults
Detect
failures
No scrollbar
inputs
Jdiff Plugin
1.3.2
experienced behaviors
b
a
f
c
c
e
d
f
Record
behaviors
Jedit 4.2 Pre9
Detect
(predict)
failures
Verify
the new
system
Jedit
Diagnose
faults
legal behaviors
Heal
faults
Jdiff Plugin
1.3.2
failure
c
f
b
a
e
c
d
f
differences
experienced behaviors
Jedit 4.2 Pre9
b
a
findScrollBar.returnValue != null
f
c
c
e
d
f
Jedit: fault localization
findScrollBar.returnValue != null
Faulty findScrollBar
Aelfred XML Parser
generate information for fault diagnosis
legal behaviors
Aelfred XML
Parser
b
a
test
cases
Jedit
f
c
c
e
d
f
Detect
(predict)
failures
Verify
the new
system
Aelfred XML Parser
Diagnose
faults
Failure condition:
Unhandled exception
Heal
faults
Detect
failures
Unhandled exception
inputs
Aelfred XML
Parser
experienced behaviors
b
a
f
c
c
e
d
f
Record
behaviors
PtPlot
Detect
(predict)
failures
Aelfred XML Parser
Verify
the new
system
Diagnose
faults
Heal
faults
legal behaviors
failure
Aelfred XML
Parser
c
f
b
a
e
c
d
f
differences
PtPlot
experienced behaviors
b
“exception”
a
f
c
c
e
d
f
Aelfred XML Parser
“exception”
Faulty method/exception handler
What’s next
• Failure detection
– What are the right models?
• Dynamic analysis support fault diagnosis
– How can we generalize?
• fault taxonomies to identify fixing strategies
– What are interesting fault taxonomies
Your input is greatly appreciated!