Transcript HCES-May-01-3 - Kansas State University

Tool-supported Program Abstraction
for Finite-state Verification
Matthew Dwyer1, John Hatcliff1, Corina Pasareanu1,
Robby1, Roby Joehanes1, Shawn Laubach1,
Willem Visser2, Hongjun Zheng1
Kansas State University1
NASA Ames Research Center/RIACS2
http://www.cis.ksu.edu/santos/bandera
Abstraction: the key to scaling up
represents a
set of states
symbolic state
abstraction
Original
system
Abstract
system
Safety: The set of behaviors of the abstract system over-approximates
the set of behaviors of the original system
Goals of our work …
Develop multiple forms of tool support for abstraction that are …
… applicable to program source code
… largely automated
… usable by non-experts
Evaluate the effectiveness of this tool support through…
… implementation in the Bandera toolset
… application to real multi-threaded Java programs
Case Study: DEOS Kernel
Honeywell Dynamic Enforcement Operating System (DEOS)



A real-time operating system for integrated modular
avionics systems
Large C++ program, manually sliced and inspected
Slice translated to Java by NASA Ames
– 1443 lines of code, 20 classes, 6 threads

With a known bug
Requirement:
Application processes are guaranteed to be
scheduled for their budgeted time during a
scheduling unit
DEOS Architecture
DEOS Kernel
class Thread
Environment
class Scheduler
User Process 1
User Process 2
class StartofPeriodEvent
...
System Clock
& Timer
class ListofThreads
Requirement
Monitor
...
if(...)
assert(false);
...
Verification of DEOS

We used Bandera and Java PathFinder (JPF)
 Verification of the system exhausted 4
Gigabytes of memory without completing
– no information about satisfaction of requirement

To verify property or produce a counterexample
– state space must be reduced
– some form of abstraction is needed
Data Type Abstraction
Collapses data domains via abstract interpretation:
Code
int x = 0;
if (x == 0)
x = x + 1;
Data domains
int
(n<0) : NEG
(n==0): ZERO
(n>0) : POS
Signs x = ZERO;
if (Signs.eq(x,ZERO))
x = Signs.add(x,POS);
Signs
NEG ZERO POS
Variable Selection
Control dependencies:
DEOS Kernel
Environment
User Process 1
class Thread
16 methods
int itsLastExecution;
...
public void startChargingCPUTime(){
int cp=itsEvent.currentPeriod();
if(cp == itsLastExecution) {
... }
32 variables
class StartofPeriodEvent
User Process 2
...
System Clock
& Timer
29 conditionals
int itsPeriodId = 0;
...
public int currentPeriod() {
return itsPeriodId;
}
public void pulseEvent(...) {...
if(countDown == 0) {
itsPeriodId=itsPeriodId + 1;
... }
Requirement
Monitor
...
if(...)
assert(false);
...
Variable Selection
Control dependencies:
DEOS Kernel
Environment
User Process 1
class Thread
16 methods
int itsLastExecution;
...
public void startChargingCPUTime(){
int cp=itsEvent.currentPeriod();
if(cp == itsLastExecution) {
... }
32 variables
class StartofPeriodEvent
User Process 2
...
System Clock
& Timer
29 conditionals
int itsPeriodId = 0;
...
public int currentPeriod() {
return itsPeriodId;
}
public void pulseEvent(...) {...
if(countDown == 0) {
itsPeriodId=itsPeriodId + 1;
... }
Requirement
Monitor
...
if(...)
assert(false);
...
Variable Selection
Data dependencies
DEOS Kernel
class Thread
Environment
User Process 1
int itsLastExecution;
...
public void startChargingCPUTime(){
int cp=itsEvent.currentPeriod();
if(cp == itsLastExecution) {
... }
class StartofPeriodEvent
User Process 2
...
System Clock
& Timer
int itsPeriodId = 0;
...
public int currentPeriod() {
return itsPeriodId;
}
public void pulseEvent(...) {...
if(countDown == 0) {
itsPeriodId=itsPeriodId + 1;
... }
Requirement
Monitor
...
if(...)
assert(false);
...
Unbounded!
Attaching Abstract Types
DEOS Kernel
class Thread
Environment
User Process 1
SIGNS
int itsLastExecution;
...
public void startChargingCPUTime(){
SIGNS
int cp=itsEvent.currentPeriod();
if(cp == itsLastExecution) {
... }
class StartofPeriodEvent
User Process 2
...
System Clock
& Timer
SIGNS
int itsPeriodId = 0;
...
public int currentPeriod() {
return itsPeriodId;
}
public void pulseEvent(...) {...
if(countDown == 0) {
itsPeriodId=itsPeriodId + 1;
... }
Requirement
Monitor
...
if(...)
assert(false);
...
Code Transformation
DEOS Kernel
class Thread
Environment
User Process 1
Signs itsLastExecution;
...
public void startChargingCPUTime(){
Signs cp=itsEvent.currentPeriod();
if(Signs.eq(cp,itsLastExecution)){
... }
class StartofPeriodEvent
User Process 2
...
System Clock
& Timer
Signs itsPeriodId = ZERO;
...
public Signs currentPeriod() {
return itsPeriodId;
}
public void pulseEvent(...) {...
if(countDown == 0) {
itsPeriodId=Signs.add(itsPeriodId
,POS);... }
Requirement
Monitor
...
if(...)
assert(false);
...
Verification of Abstracted DEOS

JPF completed the check
– produced a 464 step counter-example

Does the counter-example correspond to a
feasible execution?
– difficult to determine
– because of abstraction, we may get spurious errors

We re-ran JPF to perform a customized search
– found a guaranteed feasible 318 step counter-example
Our hypothesis
Abstraction of data domains is necessary
Automated support for
–
–
–
–
Defining abstract domains (and operators)
Selecting abstractions for program components
Generating abstract program models
Interpreting abstract counter-examples
will make it possible to
– Scale property verification to realistic systems
– Ensure the safety of the verification process
Bandera
Abstraction
Specification
Abstraction in Bandera
Language
Variable
x
y
done
count
….
o
b
Concrete Abstract Inferred
Type
Type
Type
int
int
bool
int
Object
Buffer
Program
Signs
Signs
Signs
bool
int
….
Point
Buffer
Abstract Code
Generator
PVS
Abstraction
Definition
Abstraction
Library
Abstracted
Program
BASL
Compiler
Definition of Abstractions in BASL
abstraction Signs abstracts int
begin
TOKENS = { NEG, ZERO, POS };
abstract(n)
begin
n < 0
n == 0
n > 0
end
-> {NEG};
-> {ZERO};
-> {POS};
Automatic
Generation
operator + add
begin
(NEG , NEG) -> {NEG} ;
(NEG , ZERO) -> {NEG} ;
(ZERO, NEG) -> {NEG} ;
(ZERO, ZERO) -> {ZERO} ;
(ZERO, POS) -> {POS} ;
(POS , ZERO) -> {POS} ;
(POS , POS) -> {POS} ;
(_,_) -> {NEG,ZERO,POS};
/* case (POS,NEG),(NEG,POS) */
end
Example: Start safe, then refine: +(NEG,NEG)={NEG,ZERO,POS}
Proof obligations submitted to PVS...
Forall n1,n2: neg?(n1) and neg?(n2) implies not pos?(n1+n2)
Forall n1,n2: neg?(n1) and neg?(n2) implies not zero?(n1+n2)
Forall n1,n2: neg?(n1) and neg?(n2) implies not neg?(n1+n2)
Compiling BASL Definitions
abstraction Signs abstracts int
begin
TOKENS = { NEG, ZERO, POS };
abstract(n)
begin
n < 0
n == 0
n > 0
end
-> {NEG};
-> {ZERO};
-> {POS};
public class Signs {
public static final int NEG = 0; // mask 1
public static final int ZERO = 1; // mask 2
public static final int POS = 2; // mask 4
public static int abs(int n) {
if (n < 0) return NEG;
if (n == 0) return ZERO;
if (n > 0) return POS;
}
operator + add
public static int add(int arg1, int arg2) {
begin
Compiled if (arg1==NEG && arg2==NEG) return NEG;
(NEG , NEG) -> {NEG} ;
if (arg1==NEG && arg2==ZERO) return NEG;
(NEG , ZERO) -> {NEG} ;
if (arg1==ZERO && arg2==NEG) return NEG;
(ZERO, NEG) -> {NEG} ;
if (arg1==ZERO && arg2==ZERO) return ZERO;
(ZERO, ZERO) -> {ZERO} ;
if (arg1==ZERO && arg2==POS) return POS;
(ZERO, POS) -> {POS} ;
if (arg1==POS && arg2==ZERO) return POS;
(POS , ZERO) -> {POS} ;
if (arg1==POS && arg2==POS) return POS;
(POS , POS) -> {POS} ;
return Bandera.choose(7);
(_,_)-> {NEG, ZERO, POS};
/* case (POS,NEG), (NEG,POS) */
/* case (POS,NEG), (NEG,POS) */
}
end
Data Type Abstractions
 Library of abstractions for base types
contains:
– Range(i,j), i..j modeled precisely, e.g., Range(0,0) is
the signs abstraction
– Modulo(k), Set(v,…)
– Point maps all concrete values to unknown
– User extendable for base types

Array abstractions: index & element abstractions
 Class abstractions: abstract each field
Interpreting Results

For an abstracted program, a counter-example
may be infeasible because:
– Over-approximation introduced by abstraction

Example:
x = -2; if(x + 2 == 0) then ...
x = NEG; if(Signs.eq(Signs.add(x,POS),ZERO)) then ...
{NEG,ZERO,POS}
Choose-free state space search

Theorem [Saidi:SAS’00]
Every path in the abstracted program where all
assignments are deterministic is a path in the
concrete program.

Bias the model checker
– to look only at paths that do not include
instructions that introduce non-determinism

JPF model checker modified
– to detect non-deterministic choice (i.e. calls to
Bandera.choose()); backtrack from those
points
Choice-bounded Search
State space searched
choose()
X
X
Comparison to Related Work

Predicate abstraction (Graf/Saidi)
– We use PVS to abstract operator definitions, not
complete systems
– We can reuse abstractions for different systems

Tool support for program abstraction
– e.g., SLAM, JPF, Feaver

Abstraction at the source-code level
– Supports multiple checking tools
– e.g., JPF, Java Checker/Verisoft, FLAVERS/Java, …

Counter-example analysis
– Theorem prover based (InVest)
– Forward simulation (Clarke et. al.)
Status

Bandera supports abstraction
– Library of base type abstractions
– Tool-support for user-defined abstraction
– Array abstractions
– Finding feasible counter-examples

Surprisingly effective on realistic code
– 1000s of lines, 10s of threads
– Non-trivial data that influences control
Ongoing Work

Extending abstractions
– Heap abstractions
– Symbolic abstractions

Automated support for selection
– Counter-example driven refinement

Environments and abstraction
 Discrete-time abstractions
– Exploit scheduling information from RT Java