Transcript Slide

IWFST, Shanghai, China, 2005.11.08.
Model Checking for Simple Java Programs
Taehoon Lee, Gihwon Kwon
Department of Computer Science
Kyonggi University , Korea
Verification
Does system satisfy requirements?
system
requirement
?
yes
Model checking
system
modeling
no + why
model
requirement
property
specification
property
model checking
yes
2
no + why
JAMES
• Java Application Model checking Embedded Software
 JAMES.abs: abstraction module
 JAMES.mc: model checking module
JAMES.mc
JAMES.abs
Java
program &
Predicates
Abstraction
CTL logic
Theorem
Prover
3
Boolean
Program
Model
checking
True
Counter
Example
JAMES.abs
public void main( ){
1. public void main( ){
Predicate C1: m<=10;
Predicate C2: x==0;
Predicate C3: r==true;
int m = 0;
int x = 0;
boolean r = false;
2.
3.
4.
C1 = true;
C2 = true;
C3 = false;
while( !r ){
5.
6.
7.
8.
9.
10.
L1:
if( * ){
assume( !(C3));
if( * ){
assume( C1);
C1 = select(false, !C1);
}else {
assume( !(C1));
C2 = false;
C3 = true;
}
goto L1;
}
if(m <= 10){
m++;
}else{
x = 1;
r = true;
}
}
}
Predicate C1: m <= 10;
Predicate C2: x == 0;
Predicate C3: r == true;
11.
12.
13.
14.
15.
4
}
JAMES.mc
1. public void main( ){
1
Predicate C1: m <= 10;
Predicate C2: x == 0;
Predicate C3: r == true;
2.
3.
4.
C1 = true;
C2 = true;
C3 = false;
5.
6.
7.
8.
9.
10.
L1:
if( * ){
assume( !(C3));
if( * ){
assume( C1);
C1 = select(false, !C1);
}else {
assume( !(C1));
C2 = false;
C3 = true;
}
goto L1;
}
11.
12.
13.
14.
15.
5
}
2
(2, {(T , T , T )})
3
(3, {(T , T , T )})
4
(4, {(T , T , F )})
5
(5,{(T , T , F ),
)})(*, T , F ),
)})
( F , F , T )})
6
(6,{(T , T , F )})
), (*, T , F ),
)})( F , F , T )})
15
(15, {( F , F , T )})
7
(7, {(T , T , F ),
)})
(*, T , F )})
8
(8, {(T , T , F )})
), (*, T , F )})
(11,{( F , T , F )})
11
9
(9,{(T , T , F )})
(12, {( F , F , F )})
12
10
(10,{(*, T , F )})
(13, {( F , F , T )})
13
14
(14,{(*, T , F )})
), ( F , F , T )})
Results and Discussion
• Application results
 JAMES was applied to verify LEGO robot programs in Java
 Two properties were verified successfully
1) AG L1 : ( game " Clear " )
2) AG ( L 2 : ( sens ing  true)  AF L3 : (lr _ cycle _ cnt  ))
• Limitations
 No support for abstraction refinement
 No support for dynamic constructs in Java
• Discussion topics




6
How to find a good initial set of predicates in predicate abstraction ?
How to reduce iteration times in abstraction-checking-refinement ?
Which abstraction techniques are good for Java ?
How to deal with dynamic constructs in Java ?