Transcript Rockwell-Collins-Bandera-Overview

Model-checking Concurrent Java Software
Using the Bandera Tool Set
SAnToS Laboratory, Kansas State University, USA
(http://www.cis.ksu.edu/santos/bandera)
Faculty
Matthew Dwyer
John Hatcliff
Funding
Students and Post-docs
Radu Iosif
Yu Chen
Georg Jung
Todd Wallentine
US National Science Foundation (NSF)
US National Aeronautics and Space Agency (NASA)
US Department of Defense
Advanced Research Projects Agency (DARPA)
US Army Research Office (ARO)
Robby
Roby Joehanes
Venkatesh Ranganath
Oksana Tkachuk
Rockwell-Collins ATC
Honeywell Technology Center and NASA Langley
Sun Microsystems
Goals of the Project
I. Provide platform for construction of and experimentation with
technologies for model-checking concurrent Java software
… model-reduction techniques
e.g., abstraction, slicing,
compiler-based optimizations
… model-checking engines
e.g., explicit-state, symbolic
… property specification languages
e.g., temp logic, state machines
II. Integration with commonly used design notations, methods, and processes
… UML artifacts, JML
e.g., checking, specification
… automatic generation of
synchronization code with
dedicated checking
… integration with development
and certification of safety-critical
systems.
III. Evaluation using safety-critical military and civilian applications as well as
non-critical popular open-source software
Model Checking
OK
Finite-state model
or
Model Checker
(F
W)
Temporal logic formula
Error trace
Line
Line
Line
Line
Line
Line
…
Line
Line
5: …
12: …
15:…
21:…
25:…
27:…
41:…
47:…
What makes model-checking
software difficult?
OK
Finite-state model
(F
W)
or
Error trace
Model Checker
Line
Line
Line
Line
Temporal logic formula
5: …
12: …
15:…
21:…
Problems using existing checkers:

Model construction

State explosion

Property specification

Output interpretation
Model Construction Problem
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Program

Gap
Model Checker
Model Description
Semantic gap:
Programming Languages
methods, inheritance, dynamic creation, exceptions, etc.
Model Description Languages
automata
What makes model-checking
software difficult?
OK
Finite-state model
(F
W)
or
Error trace
Model Checker
Line
Line
Line
Line
Temporal logic formula
5: …
12: …
15:…
21:…
Problems using existing checkers:

Model construction

State explosion

Property specification

Output interpretation
Property Specification Problem

Difficult to formalize a requirement in
temporal logic
“Between the window open and the window
close, button X can be pushed at most twice.”
…is rendered in LTL as...
[]((open /\ <>close) ->
((!pushX /\ !close) U
(close \/ ((pushX /\ !close) U
(close \/ ((!pushX /\ !close) U
(close \/ ((pushX /\ !close) U
(close \/ (!pushX U close))))))))))
Property Specification Problem
Forced to state property in terms of model rather than source:

We want to write source level specifications...
Heap.b.head == Heap.b.tail

We are forced to write model level specifications...
(((_collect(heap_b) == 1)\
&& (BoundedBuffer_col.instance[_index(heap _b)].head ==
BoundedBuffer_col.instance[_index(heap _b)].tail) )\
|| ((_collect(heap _b) == 3)\
&& (BoundedBuffer_col_0.instance[_index(heap _b)].head ==
BoundedBuffer_col_0.instance[_index(heap _b)].tail) )\
|| ((_collect(heap _b) == 0) && TRAP))
Property Specification Problem
Complications due to the dynamic nature of OO software…
Consider multiple instances of a bounded buffer class...
Requirement:
If a buffer instance becomes full,
it will eventually become non-full.
In general, a heap object has no program-level name that
persists throughout the lifetime of the object.
b1
b2
b3
Variables
Heap object
What makes model-checking
software difficult?
OK
Finite-state model
(F
W)
or
Error trace
Model Checker
Line
Line
Line
Line
Temporal logic formula
5: …
12: …
15:…
21:…
Problems using existing checkers:

Model construction

State explosion

Property specification

Output interpretation
State Explosion Problem

Cost is exponential in the number of
components
Bit x1,…,xN

2^N states
Moore’s law and algorithm advances can help
– Holzmann: 7 days (1980) ==> 7 seconds (2000)

Explosive state growth in software
limits scalability
What makes model-checking
software difficult?
OK
Finite-state model
(F
W)
or
Error trace
Model Checker
Line
Line
Line
Line
Temporal logic formula
5: …
12: …
15:…
21:…
Problems using existing checkers:

Model construction

State explosion

Property specification

Output interpretation
Output Interpretation Problem
Line
Line
Line
Line
Line
Line
…
Line
Line
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Program
Gap
Model Description

Raw error trace may be 1000’s of steps long
Must map line listing onto model description

Mapping to source is made difficult by

5: …
12: …
15:…
21:…
25:…
27:…
41:…
47:…
Error trace
– Semantic gap & clever encodings of complex features
– multiple optimizations and transformations
Bandera:
An open tool set for model-checking Java source code
Graphical User Interface
Optimization Control
Checker
Inputs
Bandera
Temporal
Specification
Model
Checkers
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Transformation &
Abstraction Tools
Java Source
Error Trace Mapping
Bandera
Checker
Outputs
Addressing the
Model Construction Problem
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Java Source
Static Analyses
Abstract Interpretation
Slicing
Optimizations
Model Compiler
Model Description
Model extraction: compiling to model checker inputs:

Numerous analyses, optimizations,
two intermediate languages, multiple back-ends
 Slicing, abstract interpretation, specialization
 Variety of usage modes: simple...highly tuned
Addressing the
Property Specification Problem
An extensible language based on field-tested temporal
property specification patterns
[]((open /\ <>close) ->
((!pushX /\ !close) U
(close \/ ((pushX /\ !close) U
(close \/ ((!pushX /\ !close) U
(close \/ ((pushX /\ !close) U
(close \/ (!pushX U close))))))))))
Using the pattern system: 2-bounded existence
Between {open} and {close}
{pushX} exists atMost {2} times;
Addressing the
State Explosion Problem
Property
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
…
Java Source
Model Compiler
Model Descriptions
Generate models customized wrt property!

Result: multiple models --- even as many as
one per property
 Aggressive customization via slicing, abstract
interpretation, program specialization
Addressing the
Output Interpretation Problem
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Model
Description
Intermediate Representations
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Java Source
Model
Checker
Model Compiler
+ simulator
Error trace
Like a debugger: error traces mapped back to source

Run error traces forwards and backwards
 Program state queried
 Heap structures navigated
 Locks, wait sets, blocked sets displayed
Line
Line
Line
Line
5: …
12: …
15:…
21:…
Bandera Architecture
Property Tool
Abstraction
Analyses Engine
BIRC
Translators
BIR
SPIN
dSPIN
Java
Jimple
Parser
SMV
Slicer
Error Trace Display
Simulator
JPF
Bounded Buffer
class BoundedBuffer {
Object [] buffer;
int head;
/* next available slot */
int tail;
/* last available slot */
int bound; /* max # of elements
*/
public BoundedBuffer(int b)
{…}
Initialization
head
tail
Add,Add
head
tail
public synchronized boolean isEmpty()
{…}
public synchronized void add(Object o)
{…}
public synchronized Object take ()
{…}
}
Add,Take,Take
tail head
Property Specification
/**
* @observable
*
EXP Full: (head == tail);
*/
class BoundedBuffer {
Object [] buffer;
int head, tail, bound;
public synchronized
void add(Object o)
{…}
public synchronized
Object take ()
{…}
}
Requirement:
If a buffer becomes full,
it will eventually become
non-full.
Bandera Specification:
FullToNonFull:
forall[b:BoundedBuffer].
{Full(b)} leads to
{!Full(b)} globally;
Property Specification
/**
* @observable
* EXP Empty:
* head == ((tail+1) % bound);
*/
class BoundedBuffer {
int head, tail, bound;
/**
* @observable INVOKE Call;
*/
public synchronized
void add(Object o)
{…}
/**
* @observable RETURN Return;
*/
public synchronized
Object take ()
{…}
}
Requirement:
Empty buffers must
added to before being
taken from
Bandera Specification:
NoTakeWhileEmpty:
forall[b:BoundedBuffer].
{take.Return(b)} is absent
after {Empty(b)}
until {add.Call(b)};
Property-directed Slicing
indirectly
relevant
Slice
mentioned
in property
Source program
Resulting
slice

slicing criterion generated automatically from
observables mentioned in the property
 backwards slicing automatically finds all
components that might influence the observables.
Property-directed Slicing
/**
* @observable EXP Full: (head == tail)
*/
class BoundedBuffer {
Object [] buffer_;
int bound;
int head, tail;
Slicing Criterion
All statements
that assign to
head, tail.
removed by
slicing
public synchronized void add(Object o) {
while ( tail == head )
try { wait(); } catch ( InterruptedException ex) {}
buffer_[head] = o;
head = (head+1) % bound;
notifyAll();
}
...
}
Included in
slicing
critirion
indirectly
relevant
Abstraction Engine
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 (x == zero)
x = pos;
Signs
neg zero pos
Abstraction Component
Functionality
PVS
Variable
x
y
done
count
….
o
b
Concrete Abstract Inferred
Type
Type
Type
int
int
bool
int
Signs
Object
Buffer
Jimple
Jimple
Signs
Signs
Bool
intAbs
….
Point
Buffer
BASL
Compiler
Bandera
Abstraction
Specification
Abstraction
Library
Abstraction
Engine
Language
Abstracted
Jimple
Abstraction Specification
abstraction Signs abstracts int
begin
TOKENS = { NEG, ZERO, POS };
abstract(n)
begin
n < 0
n == 0
n > 0
end
-> {NEG};
-> {ZERO};
-> {POS};
operator + add
Compiled
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
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 abstract(int n) {
if (n < 0) return NEG;
if (n == 0) return ZERO;
if (n > 0) return POS;
}
public static int add(int arg1, int arg2) {
if (arg1==NEG && arg2==NEG) return NEG;
if (arg1==NEG && arg2==ZERO) return NEG;
if (arg1==ZERO && arg2==NEG) return NEG;
if (arg1==ZERO && arg2==ZERO) return ZERO;
if (arg1==ZERO && arg2==POS) return POS;
if (arg1==POS && arg2==ZERO) return POS;
if (arg1==POS && arg2==POS) return POS;
return Bandera.choose(7);
/* case (POS,NEG), (NEG,POS) */
}
Specification Creation Tools
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};
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)
Bounded Buffer BIR
State Declarations
process BoundedB()
BoundedBuffer_rec
= record {
bound : range -1..4;
head : range -1..4;
tail : range -1..4;
BIRLock : lock wait reentrant;
};
static identification of threads
object state as record
bounded integer values
qualified lock representation
BoundedBuffer_col :
collection [3] of BoundedBuffer_rec;
BoundedBuffer_col_0 : collection [3] of BoundedBuffer_rec;
BoundedBuffer_ref =
ref { BoundedBuffer_col,
BoundedBuffer_col_0 };
“mini-heaps”
– one per allocator site
Reference type indicates mini-heaps
that can be pointed to.
Easily express results of “points-to”
analysis
Bounded Buffer BIR
Guarded Transitions
loc s34:
live { b2, b1, T_0, T_6, T_8 }
when true
do invisible {
T_8 := (T_6 % T_8);
} goto s35;
…
loc s36:
live { b2, b1, T_0 }
when true do {
notifyAll(T_0.BIRLock);
} goto s37;
…
loc s37:
live { b2, b1, T_0 }
when true do {
unlock(T_0.BIRLock);
} goto s38;
control point label
live variable information
used to optimize back-end code
annotation denoting
invisible transition which can
be merged with following
transition
built-in operations on
lock representations
Case Study: DEOS Kernel (with NASA Ames)
Honeywell Dynamic Enforcement Operating System (DEOS)



A real-time operating system for integrated modular
avionics systems
Some interesting history…
Non-trivial concurrent Java program: 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 counter-example
– to reduce the state space to a tractable size
– some form of abstraction is needed
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

After fixing the bug
– the requirement was verified
Summary

A collection of tools for reasoning about concurrent systems.

Has been applied to find bugs in safety-critical systems.
– Can it be used effectively by others – people familiar with quality
assurance issues?

Still a research prototype, but the implementation is maturing.

Is it possible to integrate tools like this into the develop process for
certified systems?
– As a simple debugging utitlity?
– As an officially sanctioned (certified) tool?
– Can it complement existing tools used in certification – especially when
concurrency is considered?

The JPF back-end has been modified to produce coverage information.
– Can this complement existing coverage tools?

We would be happy to have challenge problems/case studies.
Primary Challenges
Unclear how far model-checking can be pushed
down the hierarchy of software developers




Will there be so much technical knowledge and effort required that it
will only be used by research teams or quality assurance in highly
safety-critical applications?
Can it be integrated well enough with standard development
processes so it can be used not only with designs but also mesh
well with rigorous testing?
Can software engineers be trained in the concepts of abstraction
and temporal logic, e.g., in a one semester course, so with little
further training they can use tools effectively, in concurrent software
development?
Can effective “canned” solutions be provided for particular
application domains – thus enabling developers with less training?