# Presentation: 933177

## Software Model Checking

- Willem Visser
- Research Institute for Advanced Computer Science
- NASA Ames Research Center
- wvisser@email.arc.nasa.gov

## Overview

- Introduction to Model Checking
- Hardware and Software Model Checking
- Program Model Checking
- Major Trends
- Abstraction
- Improved model checking technology
- A Brief History
- SPIN
- Hand-translations
- State-less model checking
- Semi-automated translations
- Fully automated translations
- Current Trends
- Custom-made model checkers for programs
- SLAM
- JPF
- Summary
- NASA Case Studies - Remote Agent, DEOS and Mars Rover
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## Model Checking The Intuition

- Calculate whether a system satisfies a certain behavioral property:
- Is the system deadlock free?
- Whenever a packet is sent will it eventually be received?
- So it is like testing? No, major difference:
- Look at *all* possible behaviors of a system
- Automatic, if the system is finite-state
- Potential for being a push-button technology
- Almost no expert knowledge required
- How do we describe the system?
- How do we express the properties?

- © Willem Visser 2002

- 24 September 2002

## Labeled State GraphKripke Structure

- K = ({p,~p},{x,y,z,k,h},R,{x},L)

- Each state represents all
- variable values and location counters

- The labels representpredicates in each statee.g. (x = 5)

- Each transition represents an execution step in the system

- © Willem Visser 2002

- 24 September 2002

## Property Specifications

- Linear Time
- Every moment has a unique successor
- Infinite sequences (words)
- Linear Time Temporal Logic (LTL)

- Branching Time
- Every moment has several successors
- Infinite tree
- Computation Tree Logic (CTL)

-  Temporal Logic
-  Express properties of event orderings in time
-  e.g. “Always” when a packet is sent it will “Eventually”  be received

- © Willem Visser 2002

- 24 September 2002

## Safety and Liveness

- Safety properties
- Invariants, deadlocks, reachability, etc.
- Can be checked on finite traces
- “something bad never happens”
- Liveness Properties
- Fairness, response, etc.
- Infinite traces
- “something good will eventually happen”

- © Willem Visser 2002

- 24 September 2002

## Mutual Exclusion Example

-  Two process mutual exclusion with shared semaphore
-  Each process has three states
-  Non-critical (N)
-  Trying (T)
-  Critical (C)
-  Semaphore can be available (S0) or taken (S1)
-  Initially both processes are in the Non-critical state and   the semaphore is available --- N1 N2 S0

- © Willem Visser 2002

- 24 September 2002

## Mutual Exclusion Example

- N1N2S0

- C1N2S1

- T1T2S0

- N1T2S0

- T1N2S0

- N1C2S1

- T1C2S1

- C1T2S1

- K ╞ AG EF (N1  N2  S0)

*No matter where you are** **there is **always a way** **to get to the initial state*

- © Willem Visser 2002

- 24 September 2002

## Mutual Exclusion Example

- N1N2S0

- C1N2S1

- T1T2S0

- N1T2S0

- T1N2S0

- N1C2S1

- T1C2S1

- C1T2S1

- K ╞ AG EF (N1  N2  S0)

- © Willem Visser 2002

- 24 September 2002

## Mutual Exclusion Example

- N1N2S0

- C1N2S1

- T1T2S0

- N1T2S0

- T1N2S0

- N1C2S1

- T1C2S1

- C1T2S1

- K ╞ AG EF (N1  N2  S0)

- © Willem Visser 2002

- 24 September 2002

## Mutual Exclusion Example

- N1N2S0

- C1N2S1

- T1T2S0

- N1T2S0

- T1N2S0

- N1C2S1

- T1C2S1

- C1T2S1

- K ╞ AG EF (N1  N2  S0)

- © Willem Visser 2002

- 24 September 2002

## Mutual Exclusion Example

- N1N2S0

- C1N2S1

- T1T2S0

- N1T2S0

- T1N2S0

- N1C2S1

- T1C2S1

- C1T2S1

- K ╞ AG EF (N1  N2  S0)

- © Willem Visser 2002

- 24 September 2002

## Mutual Exclusion Example

- N1N2S0

- C1N2S1

- T1T2S0

- N1T2S0

- T1N2S0

- N1C2S1

- T1C2S1

- C1T2S1

- K ╞ AG EF (N1  N2  S0)

- © Willem Visser 2002

- 24 September 2002

## Model Checking

- Given a Kripke structure *M = (S,R,L)* that represents a finite-state concurrent system and a temporal logic formula *f *expressing some desired specification, find the set of states in *S* that satisfy *f*:			{ s  S | M,s ╞ f }
- Normally, some states of the concurrent system are designated as initial states. The system satisfies the specification provided all the initial states are in the set. We often write: M ╞ f

- © Willem Visser 2002

- 24 September 2002

## Explicit vs. SymbolicModel Checking 

- Explicit State
- states are enumerated on-the-fly
- Forwards analysis
- Stores visited states in a hashtable
- Characteristics
- Memory intensive
- Good for finding concurrency errors
- Short execution paths are better, but long execution paths can also be handled
- Can handle dynamic creation of objects/threads
- Mostly used in software

- Symbolic
- Sets of states are manipulated at a time
- Typically a backwards analysis
- Transition relation encoded by (some variant of) Binary Decision Diagrams (BDDs) or as a satisfiability problem
- Characteristics
- Can handle very large state spaces
- Not as good for asynchronous systems
- Cannot deal well with long execution traces
- Works best with a static transition relation, hence doesn’t deal well with dynamic creation of objects/threads
- Mostly used in hardware

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Hardware Model Checking
- Software Model Checking
- Program Model Checking
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## Hardware Model Checking 

- BDD-based model checking was the enabling technology
- Hardware is typically synchronous and regular, hence the transition relation can be encoded efficiently
- Execution paths are typically very short
- The Intel Pentium bug, was the “disaster” that got model checking on the map in the hardware industry
- What is it going to take in the software world?
- Intel, IBM, Motorola, etc. now employ hundreds of model checking experts

- © Willem Visser 2002

- 24 September 2002

## Software Model Checking

- Although the early papers on model checking focused on software, not much happened until 1997
- Until 1997 most work was on software designs
- Since catching bugs early is more cost-effective
- Problem is that everybody use a different design notation, and although bugs were found the field never really moved beyond some compelling case-studies
- Reality is that people write code first, rather than design
- The field took off when the seemingly harder problem of analyzing actual source code was first attempted

- © Willem Visser 2002

- 24 September 2002

## Program Model Checking

- Why is program analysis with a model checker so much more interesting?
- Designs are hard to come by, but buggy programs are everywhere!
- Testing is inadequate for complex software (concurrency, pointers, objects, etc.)
- Static program analysis was already an established field, mostly in compiler optimization, but also in verification.

- © Willem Visser 2002

- 24 September 2002

## The Trends in Program Model Checking

- Bringing programs to model checking
- Abstraction (including translation)
- Bringing model checking to programs
- Improve model checking to directly deal with programs as input

*Most model checkers cannot deal with the features of modern programming languages*

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Major Trends
- Abstraction
- Improved model checking technology
- A Brief History
- Current Trends
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## Program Model CheckingEnabling Technology 

- Abstraction

- Model CheckerInput

- Infinite state

- Finite state

- © Willem Visser 2002

- 24 September 2002

## Abstraction

- Model checkers don’t take real “programs” as input
- Model checkers typically work on finite state systems
- Abstraction therefore solves two problems
- It allows model checkers to analyze a notation they couldn’t deal with before, and,
- Cuts the state space size to something manageable
- Abstraction comes in three flavors
- Over-approximations, i.e. *more behaviors* are added to the abstracted system than are present in the original
- Under-approximations, i.e. *less behaviors* are present in the abstracted system than are present in the original
- Precise abstractions, i.e. *the same behaviors* are present in the abstracted and original program

- © Willem Visser 2002

- 24 September 2002

## Under-Approximation“Meat-Axe” Abstraction

- Remove parts of the program deemed “irrelevant” to the property being checked
- Limit input values to 0..10 rather than all integer values
- Queue size 3 instead of unbounded, etc.
- The abstraction of choice in the early days of program model checking – used during the translation of code to a model checker’s input language
- Typically manual, with no guarantee that the right behaviors are removed.
- Precise abstraction, w.r.t. the property being checked, may be obtained if the behaviors being removed are indeed not influencing the property
- Program *slicing* is an example of an automated  under-approximation that will lead to a precise abstraction w.r.t. the property being checked

- © Willem Visser 2002

- 24 September 2002

## Over-ApproximationsAbstract Interpretation

- Maps sets of states in the concrete program to one state in the abstract program
- Reduces the number of states, but increases the number of possible transitions, and hence the number of behaviors
- Can in rare cases lead to a precise abstraction
- Type-based abstractions
- Replace int by Signs abstraction {neg,pos,zero}
- Predicate abstraction
- Replace predicates in the program by boolean variables, and replace each instruction that modifies the predicate with a corresponding instruction that modifies the boolean.
- Automated (conservative) abstraction
- Eliminating spurious errors is the big problem
- Abstract program has more behaviors, therefore when an error is found in the abstract program, is that also an error in the original program?
- Most research focuses on this problem, and its counter-part the elimination of spurious errors, often called *abstraction refinement*

- © Willem Visser 2002

- 24 September 2002

## BringingModel Checking to Programs

- Allow model checkers to take modern programming languages as input, or, notations that are of similar expressive power
- Major hurdle is how to encode the state of the system efficiently
- Alternatively state-less model checking
- No state encoding or storing
- Almost exclusively explicit-state model checking
- Abstraction can still be used as well
- Source to source abstractions

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Major Trends
- A Brief History
- SPIN
- Hand-translations
- State-less model checking
- Partial-order reductions
- VeriSoft
- Semi-automated translations
- Fully automated translations
- Current Trends
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## The Early Years

- Hand-translation with ad-hoc abstractions
- 1980 through mid 1990s
- Semi-automated, table-driven translations
- 1998
- Automated translations still with ad-hoc abstractions
- 1997-1999
- State-less model checking for C
- VeriSoft 1997

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Major Trends
- A Brief History
- SPIN
- Hand-translations
- State-less model checking
- Partial-order reductions
- VeriSoft
- Semi-automated translations
- Fully automated translations
- Current Trends
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## SPIN Model Checker

- Kripke structures are described as “programs” in the PROMELA language
- Kripke structure is generated on-the-fly during model checking
- Automata based model checker
- Translates LTL formula to Büchi automaton
- By far the most popular model checker
- 10th SPIN Workshop to be held with ICSE – May 2003
- Relevant theoretical papers can be found here
- http://netlib.bell-labs.com/netlib/spin/whatispin.html
- Ideal for software model checking due to expressiveness of the PROMELA language
- Close to a real programming language
- Gerard Holzmann won the ACM software award for SPIN

- © Willem Visser 2002

- 24 September 2002

## Hand-Translation

-  Hand translation of program to model checker’s input notation
-  “Meat-axe” approach to abstraction
-  Labor intensive and error-prone

- © Willem Visser 2002

- 24 September 2002

## Hand-Translation  Examples

- Remote Agent – Havelund,Penix,Lowry 1997
- http://ase.arc.nasa.gov/havelund
- Translation from Lisp to Promela (most effort)
- Heavy abstraction
- 3 man months
- DEOS – Penix, Visser, *et al. *1998/1999* *
- http://ase.arc.nasa.gov/visser
- C++ to Promela (most effort in environment generation)
- Limited abstraction - programmers produced sliced system
- 3 man months

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Major Trends
- A Brief History
- SPIN
- Hand-translations
- State-less model checking
- Partial-order reductions
- VeriSoft
- Semi-automated translations
- Fully automated translations
- Current Trends
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## State-less Model Checking

- No state storing, hence no state matching
- Must limit search-depth to ensure termination
- Enabling technology is partial-order reduction
- Avoid revisiting some states
- Annotate code to allow verifier to detect “important” statements
- Communications and nondeterministic choice
- Model checker will try all interleavings of the these statements, but will consider all other statements “atomic”, i.e. the last statement in any group will be an important one.
- Examples include
- VeriSoft
- _[http://www1.bell-labs.com/project/verisoft/](http://www1.bell-labs.com/project/verisoft/)_
- Rivet
- http://sdg.lcs.mit.edu/rivet.html
- See also work by Scott Stoller
- http://www.cs.sunysb.edu/~stoller/

- © Willem Visser 2002

- 24 September 2002

## Partial-Order Reductions

- Reduce the number of interleavings of independent concurrent transitions
-  x := 1 || y := 1  where initially x = y = 0

- 11

- 00

- 01

- 10

- x := 1

- x := 1

- y := 1

- y := 1

- 11

- 00

- 01

- 10

- x := 1

- y := 1

- y := 1

- 11

- 00

- 10

- x := 1

- y := 1

- No Reductions

- Transitions Reduced

- States Reduced

- © Willem Visser 2002

- 24 September 2002

## Partial Order ReductionsBasic Ideas

- Independence
- Independent transitions cannot disable nor enable each other
- Enabled independent transitions are commutative
- Partial-order reductions only apply during the on-the-fly construction of the Kripke structure
- Based on a *selective search* principle
- Compute a subset of enabled transitions in a state to execute
- Sleep sets (Reduce transitions)
- Persistent sets (Reduce states)

- © Willem Visser 2002

- 24 September 2002

## Persistent Set Reductions

- A subset of the enabled transitions is called *persistent*, when any transition can be executed from outside the set and it will not interact or affect the transitions inside the set
- Use the static structure of the system to determine what goes into the persistent set
- Note, all enabled transitions are trivially persistent
- Only execute transitions in the persistent set
- Persistent set algorithm is used within SPIN
- See papers by Godefroid and Peled

- © Willem Visser 2002

- 24 September 2002

## VeriSoft

- The first model checker that could handle programs directly
- C programs running on Unix
- Relies on partial-order reductions to limit the number of times a state is revisited
- Persistent sets
- Reduce states visited
- Sleep sets
- Reduce transitions executed
- Paths must be replayed from the initial state to try new branches
- No check-pointing

- PersistentSets

- SleepSets

- © Willem Visser 2002

- 24 September 2002

## State-less Example

-  DFS with state storage – executes 12 transitions
-  DFS state-less – executes 24 transitions

- T1 ; T2 || T3 ; T4

- © Willem Visser 2002

- 24 September 2002

## State-less Example

-  DFS with state storage – executes 12 transitions
-  DFS state-less – executes 24 transitions
-  DFS state-less with partial-order reduction
-  Sleep sets - executes 8 transitions (all states)

- T2

- T3

- T2

- T2

- T1

- T1

- T1

- T4

- T3

- T3

- T4

- T4

- T1 ; T2 || T3 ; T4

- © Willem Visser 2002

- 24 September 2002

## State-less Example

-  DFS with state storage – executes 12 transitions
-  DFS state-less – executes 24 transitions
-  DFS state-less with partial-order reduction
-  Sleep sets - executes 8 transitions (all states)
-  Persistent sets – executes 4 transitions (only 5 states)

- T2

- T3

- T2

- T2

- T1

- T1

- T1

- T4

- T3

- T3

- T4

- T4

- T1 ; T2 || T3 ; T4

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Major Trends
- A Brief History
- SPIN
- Hand-translations
- State-less model checking
- Partial-order reductions
- VeriSoft
- Semi-automated translations
- Fully automated translations
- Current Trends
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## Semi-Automatic Translation

- Table-driven translation and abstraction
- Feaver system by Gerard Holzmann
- User specifies code fragments in C and how to translate them to Promela (SPIN)
- Translation is then automatic
- Found 75 errors in Lucent’s PathStar system
-  _[http://cm.bell-labs.com/cm/cs/who/gerard/](http://cm.bell-labs.com/cm/cs/who/gerard/)_
- Advantages
- Can be reused when program changes
- Works well for programs with long development and only local changes

- © Willem Visser 2002

- 24 September 2002

## Fully Automatic Translation

- Advantage
- No human intervention required
- Disadvantage
- Limited by capabilities of target system
- Examples
- Java PathFinder 1- _[http://](http://ase.arc.nasa.gov/havelund/jpf.html)__[ase.arc.nasa.gov/havelund/jpf.html](http://ase.arc.nasa.gov/havelund/jpf.html)_
- Translates from Java to Promela (Spin)
- JCAT - http://www.dai-arc.polito.it/dai-arc/auto/tools/tool6.shtml
- Translates from Java to Promela (or dSpin)
- Bandera - http://www.cis.ksu.edu/santos/bandera/
- Translates from Java bytecode to Promela, SMV or dSpin

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Major Trends
- A Brief History
- Current Trends
- Custom-made model checkers for programs
- Abstraction
- SLAM
- JPF
- Summary
- Examples of other software analyses
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## Program Model CheckingCurrent Trends

- Custom-made model checkers for programming languages with automatic abstraction at the source code level
- Automatic abstraction & translation based transformation to new “abstract” formalism for model checker
- Abstraction refinement mostly automated

- © Willem Visser 2002

- 24 September 2002

## Custom-made Model Checkers

- Translation based
- dSpin
- Spin extended with dynamic constructs
- Essentially a C model checker
- Source-2-source abstractions can be supported
- http://www.dai-arc.polito.it/dai-arc/auto/tools/tool7.shtml
- SPIN Version 4 (not released yet)
- PROMELA language augmented with C code
- Table-driven abstractions
- Bandera
- Translated Bandera Intermediate Language (BIR) to a number of back-end model checkers, but, a new BIR custom-made model checker is under development
- Supports source-2-source abstractions as well as property-specific slicing
- http://www.cis.ksu.edu/santos/bandera/

- © Willem Visser 2002

- 24 September 2002

## Custom-made Model Checkers

- Abstraction based
- SLAM
- C programs are abstracted via predicate abstraction to boolean programs for model checking
- http://research.microsoft.com/slam/
- BLAST
- Similar basic idea to SLAM, but using *lazy* abstraction, i.e. during abstraction refinement don’t abstract the whole program only certain parts
- http://www-cad.eecs.berkeley.edu/~tah/blast/
- 3-Valued Model Checker (3VMC) extension of TVLA for Java programs
- http://www.cs.tau.ac.il/~yahave/3vmc.htm
- http://www.math.tau.ac.il/~rumster/TVLA/

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Major Trends
- A Brief History
- Current Trends
- Custom-made model checkers for programs
- Abstraction
- SLAM
- JPF
- Summary
- Examples of other software analyses
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## Abstraction

- Data type based abstractions
- Abstract Interpretation (Patrick Cousot)
- E.g. replace integer variable with odd-even range or Signs abstraction {negative,zero,positive}
- Replace all operations on the concrete variable with corresponding abstract operations
-  add(pos,pos) = pos
-  subtract(pos,pos) = negative | zero | pos
-  eq(pos,pos) = true | false
- Predicate Abstraction  (Graf, Saïdi see also Uribe)
- Create abstract state-space w.r.t. set of predicates defined in concrete system

- © Willem Visser 2002

- 24 September 2002

## Data Type Abstraction

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

**Data domains**

- int

**Code**

- Collapses data domains via abstract interpretation:

- © Willem Visser 2002

- 24 September 2002

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

## Predicate Abstraction

- EQ = T

- EQ = F

- x = 0
- y = 0

- x = 0
- y = 1

- y++

- EQ := F

- EQ (x = y)

- EQ (x = y)

-  Mapping of a concrete system to an abstract system, whose states  correspond to truth values of a set of predicate
-  Create abstract state-graph during model checking, or,
-  Create an abstract transition system before model checking

- © Willem Visser 2002

- 24 September 2002

## Example Predicate Abstraction

- Predicate: B  (x = y)

- Concrete Statement
-  y := y + 1

- Abstract Statement

- y := y + 1 {x = y}

- y := y + 1 {x  y}

-  {x  y + 1}

-  {x = y + 1}

- Step 1: Calculate pre-images

- Step 2: Rewrite in terms of predicates

- Step 2a: Use Decision Procedures

-  x = y  x = y + 1

-  x  y  x = y + 1

-  x = y  x  y + 1

-  x  y  x  y + 1

- {x = y + 1} y := y + 1 {B}
- {B}  y := y + 1 {~B}

- Step 3: Abstract Code

- IF B THEN B := false
- ELSE B := true | false

- © Willem Visser 2002

- 24 September 2002

## Example of Infeasible Counter-example

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

**Example of Infeasible Counter-example**

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

***Signs:***
**n < 0 -> neg**
**  ****0   -> zero**
**n > 0 -> pos**

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Major Trends
- A Brief History
- Current Trends
- Custom-made model checkers for programs
- Abstraction
- SLAM
- Abstraction Refinement
- JPF
- Summary
- Examples of other software analyses
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## SLAMSimplified View

- C Program
- annotated with
- API usage rules

- Correct

- Error-trace

- Predicates

- False
*Error-trace is Feasible*

- © Willem Visser 2002

- 24 September 2002

## SLAM

- Check API usage rules for sequential C programs
- Mostly applied to device driver code
- C2BP
- Inputs: C program and predicates
- Output: boolean program over the predicates
- BEBOP
- Symbolic interprocedural data flow analysis
- Concrete CFG and BDD encoding of states
- NEWTON
- Symbolic execution of C programs
- Using Simplify theorem prover for checking feasibility of conditionals

- © Willem Visser 2002

- 24 September 2002

## Abstraction Refinement ExampleAdapted from Ball & Rajamani POPL02

- Property: *if a lock is held it must be released before reacquiring*

**do {**
**     ****//get the write lock**
**	****KeAcquireSpinLock(&devExt->writeListLock);**
**	**
**	****nPacketsOld = nPackets; **
**	****request = devExt->WLHeadVa;**
**	**
**	****if (request){**
**	****	****KeReleaseSpinLock(&devExt->writeListLock);**
**	****	****...**
**	****	****nPackets++;**
**	****}**
**} while (****nPackets != nPacketsOld****);**
**KeReleaseSpinLock(&devExt->writeListLock);**

- © Willem Visser 2002

- 24 September 2002

## Initial Abstraction and Model Checking

**[1] do**
**   ****//get the write lock**
**[2]****	****Acquire****Lock();****	****	**
**[3]****	****if (*) then****	****  **
**[4]****	****  ****ReleaseLock();****	****	**
**	****    ****fi**
**[5] while (*);**
**[6] ReleaseLock();**

**Boolean Program**

**Error-trace : 1,2,3,5,1,2**

- © Willem Visser 2002

- 24 September 2002

## Symbolic Execution

**[1] do {**
**[2]****	****KeAcquireSpinLock(&devExt->writeListLock);**
**   ****	****nPacketsOld = nPackets; **
**	****    ****request = devExt->WLHeadVa;**
**[3]****	****if (request){**
**[4]****	****  ****KeReleaseSpinLock(&devExt->writeListLock);**
**	****	****  ****...**
**	****	****  ****nPackets++;**
**	****    ****}**
**[5] } while (****nPackets != nPacketsOld****);**
**[6]**** KeReleaseSpinLock(&devExt->writeListLock);**

- Symbolic execution of 1,2,3,5,1,2 shows that when 5 is executed**nPackets == nPacketsOld**** **hence the path is infeasible.
- The predicate **nPackets == nPacketsOld** is then added and
- used during predicate abstraction

- © Willem Visser 2002

- 24 September 2002

## Next Abstraction andModel Checking

**[1] do**
**[2]****	****Acquire****Lock();****	**
**[3]   ****b = true;**** // nPacketsOld = nPackets**
**[4]****	****if (*) then****	****  **
**[5]****	****  ****ReleaseLock();**
**[6]****	****  ****b = b ? False : *;**** // nPackets++****	**
**	****    ****fi**
**[7] while (****!b****); //(nPacketsOld != nPackets)**
**[8] ReleaseLock();**

**New Predicate b : (nPacketsOld == nPackets)**

**Now property holds**

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Major Trends
- A Brief History
- Current Trends
- Custom-made model checkers for programs
- SLAM
- JPF
- Abstractions
- Partial-order and symmetry reductions
- Heuristics
- New Stuff
- Summary
- Examples of other software analyses
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## Java PathFinder (2)Direct Approach

- Based on custom-made Java Virtual Machine
- Handle all of Java, since it works with bytecodes
- Written in Java
- Efficient encoding of states
- Modular design for easy extensions
- Supports LTL checking with properties expressed in Bandera’s BSL notation
- Incorporates a number of search strategies
- DFS, BFS, A*, Best-first, etc.
- Supports source-2-source abstractions
- http://ase.arc.nasa.gov/jpf

- © Willem Visser 2002

- 24 September 2002

## Java PathFinder (JPF)

- © Willem Visser 2002

- 24 September 2002

## Bandera & JPF Architecture

- BIRC

- BIR

- Simulator

- Translators

- SPIN

- dSPIN

- SMV

- © Willem Visser 2002

- 24 September 2002

**Notes:**
Now, you seen the main idea of Bandera, as time permits, I’ll show you the details of the internal architecture.
Just like a compiler, Bandera is organized into a front-end, a middle-end, and a back-end.  For each of these, we have the code flowing from front to back, but we’ll also have error trace information flowing from back to front.
<click>The Bandera front end translates Java source into a 3-address code intermediate language called Jimple.  Jimple is part of a Java compiler infrastructure developed by Laurie Hendren’s Sable group at the University of McGill.   The front end also includes a tool for declaring observable features of the source code which we’ll use in our temporal property specs, and there are also data structures required for the error trace display.
<click>The middle-end includes standard data and control-flow analyses including a flexible points-to analysis, as well as the slicing and abstraction components.
<click>The back includes a translation from Jimple to our low-level intermediate representation called BIR.  I’ll show you more about BIR later.  In this diagram you also see the simulator for BIR that’s used to generate the error trace information.
 <click>Finally, we have four checkers plugged into the back-end and now you can see the rationale for BIR --- to incorporate a new model-checker, you only need to write a translator to the model-checker’s input from BIR.
Time: 2 minutes 

## Key Points

- Models can be infinite state
- Unbounded objects, threads,...
- Depth-first state generation (explicit-state)
- Verification requires abstraction
- Handle full Java language
- but only for closed systems
- Cannot handle native code
- no Input/output through GUIs, files, Networks, ...
- Must be modeled by java code instead
- Allows Nondeterministic Environments
- JPF traps special nondeterministic methods
- Checks for User-defined assertions, deadlock and LTL properties

- © Willem Visser 2002

- 24 September 2002

## Java Extensions-Verify Class-

- Used for annotations
- Atomicity
- beginAtomic(), endAtomic()
- Nondeterminism
- int random(int); boolean randomBool(); Object randomObject(String cname);
- Properties
- AssertTrue(boolean cond)
- Miscellaneous
- Dump states, print, Daikon logs, ...

- © Willem Visser 2002

- 24 September 2002

## JPF Technologies

- Predicate abstraction and type based abstractions
- Partial order and symmetry reductions
- Slicing
- Heuristic Search
- New Stuff
- Symbolic Execution
- Error Explanations

- © Willem Visser 2002

- 24 September 2002

## Type-based AbstractionsAbstract Interpretation

**abstraction Signs abstracts int**
**  ****TOKENS = { *****neg*****, *****zero*****, *****pos***** };**
**  **
** ****abstraction mapping:**
** **
**        ****n  <  0   -> {*****neg*****};**
**        ****n  ==  0  -> {*****zero*****};**
**        ****n  >  0   -> {*****pos*****};**

**public class Signs {**
**  ****public static final int NEG  = 0; **
**  ****public static final int ZERO = 1; **
**  ****public static final int POS  = 2; **
**  **
**  ****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 a, int b){**
**    ****int r; **
**    ****Verify.beginAtomic();**
**     ****if (a==NEG  && b==NEG)  r=NEG;**
**     ****if (a==NEG  && b==ZERO) r=NEG;**
**     ****if (a==ZERO && b==NEG)  r=NEG;**
**     ****if (a==ZERO && b==ZERO) r=ZERO;**
**     ****if (a==ZERO && b==POS)  r=POS;**
**     ****if (a==POS  && b==ZERO) r=POS;**
**     ****if (a==POS  && b==POS)  r=POS;**
**     ****else r=****Verify.choose(2)****;**
**    ****Verify.endAtomic();**** **
**    ****return r; }}**

- © Willem Visser 2002

- 24 September 2002

**Notes:**
- Syntactic difference between internal and external non-determinism

- An abstract program is obtained from the concrete program by replacing the concrete data domains with abstract data domains, and concrete primitive operations with calls to methods that implement abstract operations.
- If the abstract program satisfies the abstract property infer that the concrete program satisfies the concrete property.

## JPF Predicate Abstraction

- Annotations used to indicate abstractions
- Abstract.remove(x); Abstract.remove(y);Abstract.addBoolean(“EQ”, x==y);
- Tool generates abstract Java program
- Using Stanford Validity Checker (SVC)
- JVM is extended with nondeterminism to handle over approximation
- Abstractions can be local to a class or global across multiple classes
- Abstract.addBoolean(“EQ”, A.x==B.y);
- Dynamic predicate abstraction - works across instances

- © Willem Visser 2002

- 24 September 2002

## Partial Order Reduction in JPF

- Persistent set approach
- Find transitions that are globally independent
- Always independent of all transitions in other threads
- Requires static analysis before model checking to determine global independence
- Advanced alias analysis

- © Willem Visser 2002

- 24 September 2002

## Partial-order Reduction

**class FirstTask extends Thread {**
**   ****public void run() {**
**      ****int x; S1 s1;**
**      ****x = 1;**
**      ****s1 = new S1();**
**      ****x = 3;**
**} }**

-  **class S1 {int x;} class S2 {int y;}**
** ****public class Example {**
**   ****public static void main (String[] args) {**
**    ****FirstTask t1 = new FirstTask();**
**    ****SecondTask t2 = new SecondTask();**
**    ****t1.start(); t2.start();**
**}}**

**class SecondTask extends Thread {**
**   ****public void run() {**
**      ****int x; S2 s2;**
**      ****x = 2;**
**      ****s2 = new S2();**
**      ****x = 3;**
**} }**

-  43 states with no reduction
-  18 states with partial-order reduction
-  all statements are globally independent (safe)

- © Willem Visser 2002

- 24 September 2002

## Partial-order Reduction

**class FirstTask extends Thread {**
**   ****public void run() {**
**      ****int x; S1 s1;**
**      ****Example.x = 1;**
**      ****s1 = new S1();**
**      ****x = 3;**
**} }**

**class S1 {int x;} class S2 {int y;}**
**public class Example {**
**   ****public static int x = 10;**
**   ****public static void main (String[] args) {**
**    ****FirstTask t1 = new FirstTask();**
**    ****SecondTask t2 = new SecondTask();**
**    ****t1.start(); t2.start();**
**}}**

**class SecondTask extends Thread {**
**   ****public void run() {**
**      ****int x; S2 s2;**
**      ****Example.x = 2;**
**      ****s2 = new S2();**
**      ****x = 3;**
**} }**

-  43 states with no reduction
-  27 states with partial-order reduction
-  2 statements are not globally independent

- © Willem Visser 2002

- 24 September 2002

## Symmetry Reduction

**class FirstTask extends Thread {**
**   ****public void run() {**
**      ****S s1;**
**      ****s1 = new S1();**
**} }**

-  **class S {int x;}**
** ****public class Example {**
**   ****public static void main (String[] args) {**
**    ****FirstTask t1 = new FirstTask();**
**    ****SecondTask t2 = new SecondTask();**
**    ****t1.start(); t2.start();**
**}}**

**class SecondTask extends Thread {**
**   ****public void run() {**
**      ****S s2;**
**      ****s2 = new S2();**
**} }**

-  Map allocation to Heap    position on First Path
-  Reuse same Positions    on later paths

- © Willem Visser 2002

- 24 September 2002

## Garbage Collection

**Garbage Collection**

-  **class gc {**
**    ****public static void main (String[] args) {**
**       ****while(true) {**
**         ****System.out.println(“0”);**
** ****} } }**

-  Infinite State program
-  Garbage makes the state grow...
-  JPF supports
-  Mark-and-Sweep
-  Reference counting

- © Willem Visser 2002

- 24 September 2002

## Property-directed Slicing

**slicing criterion**** generated automatically from observables mentioned in the property**

**backwards slicing automatically finds all components that might influence the observables.**

- Source program

- © Willem Visser 2002

- 24 September 2002

## Property-directed Slicing

**/****
** ***** @observable EXP Full: (head == tail) **
***/**
**class BoundedBuffer {**
**   ****Object [] buffer_;  **
**   ****int bound;**
**   ****int head, tail;**
** **
**  **
** ****public synchronized void add(Object o) {**
**    ****while ( tail == head )**
**      ****try { wait(); } catch ( InterruptedException ex) {}**
**    ****buffer_[head] = o;**
**    ****head = (head+1) % bound;**
**    ****notifyAll();**
**   ****}**
**...**
**}**

- © Willem Visser 2002

- 24 September 2002

## Slicing in JPF

- JPF uses Bandera’s slicer
- Bandera slices w.r.t.
- Deadlock - i.e. communication statements
- Variables occurring in temporal properties
- Variables participating in race-violations
- Used with JPF’s runtime analysis
- More examples of slicing for model checking
- Slicing for Promela (Millet and Teitelbaum)
- http://netlib.bell-labs.com/netlib/spin/ws98/program.html
- Slicing for Hardware Description Languages (Shankar *et al*.)
- http://www.cs.wisc.edu/~reps/

- © Willem Visser 2002

- 24 September 2002

## Heuristic Search

- Best-First, Beam and A* Search
- Heuristics based on property
-  deadlock
- Maximize number of blocked threads
-  Assertions
- Minimize distance to assertion
- Heuristics on structure of Program
- Interleaving heuristic
- Maximize different thread scheduling
- Branch Exploration
- Maximize the coverage of new branches
- Choose-free heuristic
- Minimize non-deterministic choice
- User-defined heuristics
- Full access to JVM’s state via API
- Combine heuristics

- © Willem Visser 2002

- 24 September 2002

## 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 and backtrack from those points

- © Willem Visser 2002

- 24 September 2002

## Choose-free Heuristic

- Infeasible error elimination during abstraction
- Heuristic function returns best value for states with least number of non-deterministic choices enabled
- If no “deterministic” error exists it also searches rest of the state space

- © Willem Visser 2002

- 24 September 2002

## Test Coverage for Model Checking

- Reality check:
- Model Checkers run out of memory OFTEN!
- If no error was found, how confident can we be that none exists?
- Require coverage measure
- JPF extended with Branch coverage calculations
- Can the coverage measure guide the model checker
- Yes, as a heuristic
- Better heuristic values are given for least explored branches

- © Willem Visser 2002

- 24 September 2002

## Concurrency Bugs

- Often due to unanticipated interleaving
- Increased thread interleaving might expose them
- Interleaving heuristic
- Executions in which context is switched more often are given better heuristic values

- © Willem Visser 2002

- 24 September 2002

## Scaling Program Model CheckingError-Detection

- © Willem Visser 2002

- 24 September 2002

## JPF Most Recent Extensions

- Symbolic execution based model checking
- Sarfraz Khurshid (MIT), Corina Pasareanu and Doron Peled (Warwick)
- Traverses all paths and collects and solves constraints on-the-fly during model checking
- Using the Omega libraries for constraint solving
- Main application is test-case generation
- Error Explanations
- Alex Groce (CMU)
- Find an error, then try and find “similar” paths that lead to errors (negatives) and that don’t lead to an error (positives).
- Analyze the positives and negatives
- Find smallest change to make a positive a negative
- Find invariants on positives and negatives (using Diakon)
- Find statements that are on all and only positives (negatives)

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Major Trends
- A Brief History
- Current Trends
- Custom-made model checkers for programs
- SLAM
- JPF
- Summary
- Examples of other software analyses
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## Software Model CheckingExecutive summary

- Model checking by itself cannot deal with the complexity of software
- Techniques from static analysis are required
- Abstract interpretation, slicing, alias&shape analysis, symbolic execution
- Even then, we need to borrow some more!
- Heuristic search, constraint solving, etc.
- Abandon soundness
- Aggressive heuristics
- Runtime analysis and runtime monitoring

- © Willem Visser 2002

- 24 September 2002

##  More Software Analysis TechniquesA small sample

- Program Verification
- For example, ESC/Java from Compaq
- http://research.compaq.com/SRC/esc/
- Static analysis for runtime errors
- For example, PolySpace for C, Ada and Java
- http://www.polyspace.com/
- Requirements and Design Analysis
- Analysis for SCR, RSML, Statecharts, etc.
- Runtime analysis
- See Runtime Verification Workshops
- http://ase.arc.nasa.gov/rv2002/
- Analysis Toolsets
- IF (Verimag), SAL (SRI), etc.

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Case Studies
- Remote Agent
- DEOS
- Mars Rover
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## Case Studies

***DEOS***

***Remote Agent***

***Mars Rover***

- © Willem Visser 2002

- 24 September 2002

## Case Study:DS-1 Remote Agent

- Several person-months to create verification model.
- One person-week to run verification studies.

**Tasks**

**Properties Monitor**

- Spacecraft

- Commands

- Achieve
- Property

**Change**
**Event**

- Lock
- Event

**Interrupt**

- Sensors

- Subscribe

- © Willem Visser 2002

- 24 September 2002

**Notes:**
For model-based autonomous systems, such as the Remote Agent (RA) of Deep-Space 1, analytic verification has been applied to find faults that are very difficult to find through conventional testing.
This application required Ph.D.-level experts in analytic verification.
Analytic verification was applied both to the automated reasoning methods and the application-specific models.

## Case Study: DS-1 Remote Agent

- Five difficult to find concurrency errors detected
- “[Model Checking] has had a substantial impact, helping the RA team improve the quality of the Executive  well beyond what would otherwise have been produced.” - RA team
- During flight RA deadlocked (in code we didn’t analyze)
- Found this deadlock with JPF

*wait*

***Unexpected timing ***
***of change event***

*check*

***DB change?***

*yes*

***no***

***Monitor Logic***

- © Willem Visser 2002

- 24 September 2002

## DEOS Operating System

- Integrated Modular Avionics (IMA)
- DEOS Guarantee Space and Time partitioning
- FAA Certification Process
- Requires Structural Testing Coverage (MC/DC)
- Inadequate for finding Time Partitioning Errors
- Timing Error not found by Testing occurred
- Behavioral Analysis of Time Partitioning
- NASA Ames and Honeywell HTC collaboration
- Model Check slice of DEOS containing timing error

- © Willem Visser 2002

- 24 September 2002

## DEOS Analysis

- Translated C++ 1-to-1 to PROMELA/SPIN (1500 lines of C++ code)
- Found the time-partitioning error without any prior knowledge, what the error was, where it was or what made it show up.
- Required very limited abstraction
- DEOS Team Reaction
- Surprised that error was found by directly checking code
- They expected NASA team to ask for smaller “slice”
- They now have their own model checking group building on our work
- Then translated DEOS to Java and applied JPF
- Backwards dependency analysis from the time partitioning assertion being checked revealed candidate variables to abstract
- Applied “range” abstraction {0,1,many} to a specific integer variable
- Too much of an over-approximation that led to many spurious errors
- However with the choose-free heuristic *the* non-spurious error was found

- © Willem Visser 2002

- 24 September 2002

## Error Trace

**Error Trace**

- Main: 5/20

- User1: 21/60

- User2: 21/60

- 8

- 0

- 20

- 40

- 60

- idle

- © Willem Visser 2002

- 24 September 2002

## Analysis of the K9 Mars Rover“The Experiment”

- Rover is 8000 lines of code with 6 threads
- heavy use of synchronization between the threads
- Complex queue manipulation
- Purpose
- Benchmark current state of the art in model checking, static analysis for runtime error detection and runtime analysis
- Use traditional testing as baseline
- Original code was in C++ that was translated to Java
- About half the code was translated to C for the static analysis that used PolySpace
- Method
- Controlled experiment: 4 groups of 2 people, each group uses one technology on the Mars rover code to find seeded bugs
- 3 versions created and each group gets 2 days/version
- Some bugs are removed/introduced between versions
- Any new bugs discovered are not fixed, only known ones

- © Willem Visser 2002

- 24 September 2002

## Analysis of the K9 Mars RoverHow did Model Checking do?

- Methodology for model checking
- Asked never to “run” the code, only model check it
- Keep the results clean from any testing influence
- Code is heavily dependent on time
- Given a gross over-approximation of time, where all time-related decisions became nondeterministic
- Found all, but one, of the known concurrency errors and some new ones
- Better than any of the other teams
- Only team that could always produce not just the error but how to get to it!
- Also found all the non-concurrency errors
- Interesting observations
- Abandoned the time abstraction within the first hour for one that is closer to real-time, but might miss errors
- It was too hard for them to determine if errors were spurious not knowing the code well enough
- Found a number of bugs in the first version, had a slow 2nd version, and then found all the remaining bugs in the 1st hour of the 3rd version
- Took them some time to get their framework setup, but once done, they were flying

- © Willem Visser 2002

- 24 September 2002

## Overview

- Introduction to Model Checking
- Program Model Checking
- Case Studies
- Future of Software Model Checking

- © Willem Visser 2002

- 24 September 2002

## The Future of Software Model Checking

- Abstraction based approaches
- Combine object abstractions (e.g. shape analysis) with predicate abstraction
- Automation is crucial
- Symbolic Execution
- Solving structural (object) and numerical constraints
- Acceleration techniques (e.g. widening)
- Model checking as a companion to testing
- Test-case generation by model checking
- Runtime monitoring and model checking
- Modular model checking for software
- Exploiting the interface between components
- Interface automata (de Alfaro  & Henzinger )
- Environment generation
- How to derive a “test-harness” for a system to be model checked
- Result representation
- Much overlooked, but without this we are nowhere!
- “Analysis is necessary, but not sufficient” – Jon Pincus

- © Willem Visser 2002

- 24 September 2002