# Presentation: 858515

## Tool-supported Program Abstraction for Finite-state Verification

- Matthew Dwyer1, John Hatcliff1, **Corina Pasareanu****1**, Robby1, Roby Joehanes1, Shawn Laubach1, Willem Visser2, Hongjun Zheng1
- Kansas State University1
- NASA Ames Research Center/RIACS2

*http://www.cis.ksu.edu/santos/bandera*

**Notes:**
This afternoon I will describe some of our recent work that is aimed at abstracting Java programs for verification.  This work has been done in the context of the Bandera project at Kansas State University.

## Finite-state Verification

**Notes:**
Within the bandera project, we are interested in applying fsv technologies to complex software systems.

In fsv, for ex in mc, we describe a program’s comput.behavior as a fs trans.system, we specify a program’s property in some complementary formalism, like temp. logic, and we check exhaustively that the prop. Holds at each state of the system.

The result of verif can be either: ok the property holds on the sys., or no, the prop.does not hold on the sys.and here is a counterex.

## Finite-state Verification

- Effective for analyzing properties of hardware systems

- Limited success due to the
- enormous state spaces
- associated with most software systems

- Recent years have seen many efforts to apply those techniques to software

- Widespread success andadoption in industry

## Abstraction: the key to scaling up

**Notes:**
Of course, most people recognize that abstraction is the key to scaling fsv tech. To reasoning about realistic programs.

Abstraction involves creation of a new sys with fewer states, were each state in the abs.sys. Is like a “symbolic” state that actually represents multiple states. A symbolic state may even repres.an infinite number of state.

When building abstractions, we want them to be safe. Safety allows us to infer that if a property is true for the abs system then the prop. Is true for the orig system.
However, because of over-approx., the ability to disprove properties is in general sacrificed.

## 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*

**Notes:**
DEOS Transition

In the next several slides, I will show how our abs tool work on a realistic case study. This will also illustrate several of the challenges in abstracting complex softw systems and our approach to addressing these challenges.

## Case Study: DEOS Kernel (NASA Ames)

- A real-time operating system for integrated modular avionics systems
- Non-trivial concurrent Java program: 1443 lines of code, 20 classes, 6 threads
- With a known bug

- Honeywell Dynamic Enforcement Operating System (DEOS)

## DEOS Architecture

- Requirement
-    Monitor

**System Clock **
**  ****& Timer**

**...**

- DEOS Kernel

**...**
**if(...)**
** ****assert(false);**
**...**

**Notes:**
The deos kernel has the typical data structures and algorithms that an os has. For ex, class scheduler implements the scheduling algorithm, there is also a class for the list of threads waiting to be scheduled. And an instance of class thread is created for each process that runs on the kernel

in order to analyze the kernel itself, additional code was written to simulate the behavior of user applications and the hardware env.

The requirement is encoded as a method that observes the states of the kernel and asserts that budgets are allocated in each scheduling unit.
Calls to this method are inserted whenever the kernel schedules an app process; this guarantees the detection of property violation 

## 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**

## Data Type Abstraction

- int x = 0;
- if (x == 0)
-   x = x + 1;

**Data domains**

**Code**

- Collapses data domains via abstract interpretation:

**Notes:**
The technique can be illustrated on this fragment of code; assume we would like to keep only enough info about x to allow the conditional test to be decided. So we only need to know if x is zero or not

for this we could use the signs abstraction that maps integers onto a set of 3 symbolic values:neg,zero,pos

we transform the code so that to operate on the abs domain and it looks like this; here the concrete type int was replaced by abs type signs, concrete constants 0 and 1 were replaced with abs ct 0 and pos; and primitive ops on ints were replaced with calls to some methods that implement the abs.ops.that manipulate abstract values. Ex : equality operator was replaced with a call to method signs.eq and + was replace by  signs.add .

So, how do we apply this abstraction technique to the DEOS example ?
We have to decide which variables to abstract, what abstrations to use and then we have to effectively transform the system to encode the abstractions.

## Variable Selection

- Requirement
-    Monitor

**System Clock **
**  ****& Timer**

**...**

**Control dependencies:**
**         ****29 conditionals**
**         ****16 methods**
**         ****32 variables**

**...**
**if(...)**
** ****assert(false);**
**...**

## Variable Selection

- Requirement
-    Monitor

**System Clock **
**  ****& Timer**

**...**

**Control dependencies:**
**         ****29 conditionals**
**         ****16 methods**
**         ****32 variables**

**...**
**if(...)**
** ****assert(false);**
**...**

**Notes:**
So first, we have to select variables for abstraction. In our approach this selection is guided by the property to be checked. This is a largely manual process that is greatly simplified by the use of the program dependence info., that is computed by another component of Bandera that also does slicing.

So for this ex, we tried to identify the vars. that influence the execution of the assertion.
Following control dependencies, we identified 29 conditionals that may be related to the exe of the assertion. Spread over....reference....
We analyzed this info and, within one hour, we were able to identify one conditional 

that seemed to influence a lot of program behavior related to the assertion

## Variable Selection

- Requirement
-    Monitor

**System Clock **
**  ****& Timer**

**...**

**...**
**if(...)**
** ****assert(false);**
**...**

**Data dependencies**

**Notes:**

Following data dependencies, we found that one field in another class is the source of values for the conditional. This field (itsPeriodId) is initially 0 and then it is ever incremented.

This means that it is potentially unbounded and abstracting it to a finite domain may greatly reduce the state space of the system.

So we chose this field as a candidate for abstraction.

## Attaching Abstract Types

- Requirement
-    Monitor

**System Clock **
**  ****& Timer**

**...**

**...**
**if(...)**
** ****assert(false);**
**...**

**SIGNS**

**SIGNS**

**SIGNS**

**Notes:**
And we chose to abstract it using signs, because it distinguishes the initial value 0 from subsequent values. Now, we also have to abstract all the variables whose values depend on the abstracted field.

So we abstract this and also this var.

This step of propagating abstract types is automated in Bandera by a type inference algorithm.

So now that  we assigned abstract types to selected vars, we automatically transform the code to operate on the abstract types 

## Code Transformation

- Requirement
-    Monitor

**System Clock **
**  ****& Timer**

**...**

**...**
**if(...)**
** ****assert(false);**
**...**

**Notes:**

So, we replaced the concrete integer types for the selected vars with signs, and we replaced concrete primitive operations with calls to methods that implement abstract ops.

-> Now that we’ve eliminated the problem with the variables that are potentially unbounded, we can go back to verification.

## 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**

**Notes:**
Instead of analyzing the counter-ex for feasibility, we re-run Java Path Finder to do a customized search for feasible counter-examples on the fly, during verification of the abstracted program.
This resulted in a ...... 

## 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**

**Notes:**
The DEOS experience makes it clear that abstraction is necessary for model checking of realistic Java programs.  Furthermore,this experience also illustrates the need for several different forms of tool support to achieve abstraction of large programs

Link to next slide ...
Now that you’ve seen the basic steps in abstracting a program in  Bandera  I’ll give an overview of  the abstraction components starting with the user’s interface ...

## Abstraction in Bandera

- Abstraction
- Library

- Signs

- Signs

- Signs

- int

- bool

- ....

- Point

- Buffer

**Notes:**
When the abstraction component of Bandera is invoked for some program, a hierarchical table is displayed, that lists all the variables in the program along with their types. The user selects abstractions from a  library for variables that are deemed particularly relevant to the property to be checked. The selection of variables is guided by the Pd info.  

<click> So for example, assume we select Signs for x.  Once this initial selection is made, Bandera uses a type inference phase to attach abstract types to the remaining variables.  

<click>Then the abstraction code generator transforms the program into an abstracted program that operates with abstract types, as I showed on DEOS.
So one remaining issue is where do the abstractions in this library come from?
The library is populated by an expert user who defines abstractions using a special purpose language that we’ve designed called BASL.  For base types, the user only needs to specify the abstract domain and the abstraction  function, and the PVS theorem prover is used to infer the definitions of the abstract operations.  The abstractions are then compiled to a Java representation and held in the library, for reuse. 

## Definition of Abstractions in BASL

- abstraction Signs abstracts int
- begin
-   TOKENS = { NEG, ZERO, POS };
-   abstract(n)
-     begin
-         n  <  0   -> {NEG};
-         n  ==  0  -> {ZERO};
-         n  >  0   -> {POS};
-     end

-  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

**Notes:**
In BASL, we can define AI’s. an AI is a collection of 3 components : a domain of abs.values, an abstract function and a collection of abstract op., one for each primitive operation in the program.
-For example, this is the BASL representation of the signs AI, where the abstract domain is the powerset of the set of tokens.
-The abstract ops.are automatically generated using the PVS theorem prover, for example this is the abstract version of +.
-Note that abstract operations can return more than one token.This is because by abstraction, we loose info about abs.values : you will see on the next slide, that imprecision is MODELED as a non-det. choice over the values in the set. 
-So now, how do we use the theorem prover. For ex, this is how we generate the def of abs.op + applied to 2 NEG values. We start  whith set {NEG, ZERO, POS} which  is safe because it covers all the possible results of adding 2 negative numbers.
-We try to eliminate from the set the tokens that we can prove are not possible. We submit to PVS 3 implications : one for each token in the def. Here predicate NEG? ...POS? and ZERO? are defined similarly.
-So we ask PVS : is it true that  by adding 2 neg numbers we can not get a pos. number, and PVS answers yes, so we eliminate POS from the definition,....
-> same technique for all the cases!  

## Compiling BASL Definitions

**abstraction Signs abstracts int**
**begin**
**  ****TOKENS = { NEG, ZERO, POS };**
**  ****abstract(n)**
**    ****begin**
**        ****n  <  0   -> {NEG};**
**        ****n  ==  0  -> {ZERO};**
**        ****n  >  0   -> {POS};**
**    ****end**
** ****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**

**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;**
**  ****}**
**  ****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) */**
**  ****}**

**Notes:**
BASL specification are compiled into Java classes

For example, this is the Java class for the signs abstraction.

Abstract tokens are implemented as integer values.

The abstract function is straightforward.

And this is the definition of method add that implements the abstract version of +
-> we use a special method Bandera.choose the model the imprecision introduced by the abs.
-> For ex, Bandera.choose (7) will be interpreted in subsequent verification tools (i.e. JPF) as a non-deterministic    choice between the tokens encoded in the bit-vector 7, that is between NEG, ZERO, POS. 

## 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**
**Specified by an index abstraction and an element abstraction**
**Class abstractions**
**Specified by abstractions for each field  **

## Interpreting Results

**Example:**
**x = -2;     if(x + 2 == 0) then ...**
**x = NEG; if(Signs.eq(Signs.add(x,POS),ZERO)) then ...**
**                             ****{NEG,ZERO,POS}**

**For an abstracted program, a counter-example may be infeasible because:**
**Over-approximation introduced by abstraction**

**Notes:**
-> abs.program has more behaviors than the original program 

-> a counter-ex may be reported for a behavior in the abstract system not present in the original system

We developed a technique that searches for feasible counter-ex, during verification of the abstract system.  

## 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

** ****choose()**

**X**

**X**

**Notes:**
Verif. on choose free paths will report this path....

But not this paths.....

That may correspond to a feasible execution and indicates a real defect

## 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 (CMU)**

## Conclusions

**Tool support for abstraction of base and array types enables verification of real properties of real programs**
**Extend support for objects**
**Heap abstractions ****to**** ****handle an unbounded number of dynamically allocated objects**
**Extend automation**
**Automated selection**** and ****refinement**** based on counter-example analysis**

**Notes:**
Currently we are extending bandera in both these directions and we plan to report on it in the future

## Array Abstractions

**Specified by:**
**an index abstraction and **
**an element abstraction**
**Example: ****WidgetInfo wi[k]**
**use ****signs**** for index**
**use some other abstraction for ****WidgetInfo**
**Abstracted array ****awi ****has 2 elements:**
**awi[zero]**** abstracts ****wi[0]**
**awi[pos]**** summarizes info about ****wi[1] ...wi[k]**

## Property Abstraction

- System Model

- Property

## Property Abstraction

**Properties are temporal logic formulas, written in ****negational normal form.**
**Abstract propositions ****under-approximate**** the truth of concrete propositions.**
**Examples:**
**Invariance property: **
**Abstracted to: **
**Invariance property: **
**Abstracted to:**

## Related Work

**Other DEOS case studies (promela, java)**
**SLAM**
**Feaver**
**JPF Predicate Abstraction**
**Predicate abstraction in general**
**Invest/CMU**

## Interpreting Results

**    ****...**
**[1] if(Signs.gt(Signs.add(NEG,POS),ZERO))**
**    ****then**
**[2]     assert(true);**
**    ****else**
**[3]     assert(false);**
**    ****...**

**     ****...**
**[****1] if (-2 + 3 > 0) **
**    ****then**
**[2]     assert(true);**
**    ****else**
**[3]     assert(false);**
**    ****...**

- Example of Infeasible Counter-example

## Abstraction: the key to scaling up

**Notes:**
Of course, most people recognize that creating and checking abstracted models of the system is the key to scaling up.  This involves creating a new system with fewer states where each state in the abstract system is what you can think of as a “symbolic state” that actually represents multiple states (even an Infinite number) in the original system.

Property preservation.

Because of over-approximation, the ability to disprove properties is sacrificed.

Soundness, not completeness.