# Presentation: 226800

## The JPF Experience “why model checking programs is a bad idea” 

**The JPF Experience**** “why model checking programs ****is a bad idea” **

- Willem Visser
- Automated Software Engineering Group
- NASA Ames

## Experimental Evaluation of V&V Tools on Martian Rover Software

**Experimental Evaluation of V&V Tools on Martian Rover Software**

- Guillaume Brat, Dimitra Giannakopoulou, Allen Goldberg,  Klaus Havelund, Mike Lowry, Corina Pasareanu, Arnaud Venet, _Willem Visser_
- Automated Software Engineering Group
- NASA Ames

## Overview

- Experiment Goals
- Disclaimer
- K9 Mars Rover
- Experimental Setup
- Tools
- Java PathFinder (JPF)
- PolySpace Verifier
- Java PathExplorer (JPaX) and DBRover
- Observations
- Experimental Results
- What’s next?

## V&V Experiment

- Benchmark advanced V&V tools on autonomy software
- Model Checking: Java PathFinder
- Run Time Analysis: JPaX and DBRover
- Static Analysis: PolySpace
- Objectives
- Assess maturity / usability of each technology
- Compare each technology with traditional testing
- Examine whether data indicate potential synergies
- Identify gaps with respect to autonomy V&V

## Disclaimer

***Our results are (for the most part) not statistically valid***

## However

- Problem: Complexity of the Tools and Software
- Cannot get enough equally qualified participants
- We *exploited* our summer interns
- We *exploited* our group’s expertise
- We believe our results do have value
- They confirm some common beliefs
- Can serve as a point of comparison in the future

## Target system: K9 Rover

- Executes flexible plans for autonomy
- branching on state / temporal conditions
- Multi-threaded system
- communication through shared variables
- synchronization through mutexes and condition variables
- Main functionality: 8KLOC, C++

**commands**

**plans**

- Exec

**Executive**

- CondChecker

- Database

- ActionExec

- TimeChecker

## Example of Plan

- (block :id plan
-            :continue-on-failure
-            :node-list (
-             (task :id drive1
-                      :start-condition (time +1 +5)
-                      :end-condition (time +1 +30)
-                      :action BaseMove1
-                      :duration 20
-             )
-             (task :id drive2
-                      :end-condition (time +10 +16)
-                      :action BaseMove2
-                      :duration 10
-             )
-           ) )

## Code preparation

- Code translation for tool usage
- Seeded with 12 bugs extracted from developer’s CVS log
- Bugs are distributed over three versions of the software.
- Some bugs appear in multiple versions.
- Bug classification
- concurrency bugs: deadlock and data races (7/12)
- plan bugs: plan semantics violated (5/12)

- Rover
- Exec
- C++

- Developer’s
- CVS log

## Participants

- 4 teams (MC, RA, SA, TT), two members each
- graduate students proficient in formal methods
- Ames employees with extensive background in SW development
- 3-day training
- rover executive
- V&V tools to be used
- plan description and correctness semantics
- teams are “equivalent”
- teams using different technologies are in different rooms, and cannot communicate during experiment

## Experimental Methodology

- Teams use tools to find bugs in two 8 hour periods per version
- Bug reports (preliminary and final) emailed to observers

- Testing team

- observers

- Rover
- Exec V1
- Java

- MC team

- RTA team

- Rover
- Exec
- C

- SA team

- Bug
- report

- Bug
- report

## Experimental Methodology

- Bug reports are immediately analyzed and bug fixes provided
- Only email communication between participants and observers

- Testing team

- observers

- Rover
- Exec V1
- Java

- MC team

- RTA team

- Rover
- Exec
- C

- SA team

## Tools

## Java PathFinder

## Key Points

- Models can be infinite state
- Unbounded objects, threads,...
- Depth-first state generation (explicit-state)
- Heuristic search options
- Verification requires abstraction
- Handle full Java language
- but only for closed systems
- Cannot handle native code
- Allows Nondeterministic Environments
- JPF traps special nondeterministic methods
- Checks for user-defined assertions, deadlock, race violations and LTL properties

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

## Static AnalysisPolySpace Verifier

- Static analysis (using complex integer arithmetic algorithms) finds all possible run-time errors (e.g., out-of-bound array accesses, dereferencing through null pointers, illegal type conversions, invalid arithmetic conversions, overflow/underflow, and non-initialized variables), which are difficult to detect through conventional testing.

**Notes:**
This slide shows how static analysis fares compared to state-of-practice testing. Besides the explanation on the color-coding of the results of the analysis (bottom-right corner), colors in this slide mean the following:
Red refers to testing (inputs for testing, and testing phases)
Green refers to static analysis
Yellow highlights differences between these techniques. Note that the fact that the static analysis covers the same phases as testing is represented by the parallelism (I.e., same start, same end) between the two flow charts.  

Testing requires a big manual effort (test cases and drivers) and offers only partial error coverage.

Static analysis catches all run-time errors, with a minimal manual effort, and it reduces validation costs over testing by a factor of 10; results are presented with a simple color-coded scheme (orange errors are only potential errors); however, the analysis time increases exponentially in function of the error selectivity (certain errors or correct code vs. potential errors); 

## What is Runtime Analysis

- Instrument program
- Run instrumented program
- Extract execution trace
- Analyze execution trace

## PathExplorer

**PathExplorer**

**Running program**

**socket**

**Event stream**

**Observer**

## PathExplorer – the Observer

**PathExplorer – the Observer**

**Dispatcher**

**deadlock**

**datarace**

**temporal**

- paxmodules
-   module datarace =‘java pax.Datarace’;
-   module deadlock =‘java pax.Deadlock’;
-   module temporal =‘java pax.Temporal spec’;
- end

**Event**
**stream**

- warning
- ...

- warning
- ...

- warning
- ...

**...**

## Looking for the Foot PrintsInstead of for the Bug Itself

## PathExplorer – the Observer

**PathExplorer – the Observer**

**Dispatcher**

**datarace**

**deadlock**

**temporal**

- paxmodules
-   module datarace =‘java pax.Datarace’;
-   module deadlock =‘java pax.Deadlock’;
-   module temporal =‘java pax.Temporal spec’;
- end

**Event**
**stream**

- warning
- ...

- warning
- ...

- warning
- ...

**...**

## Runtime MonitoringPathExplorer/DBRover

**always**(A -> (!C **until** B))

- A

- B

- C

- B

- A

**C**

- observer

- events

- Translates into observer

**Temporal logic** facilitates
- expression of requirements
- that relate a vehicle’s states
- at different time points.

- Formalized temporal requirement

- A

## Setup & Observationsfor each technology

- Model Checking
- JPF
- Static Analysis
- PolySpace
- Runtime Analysis
- JPaX
- DBRover

## Model Checking Setup

- “Atomic” statements added
- Although JPF support partial-order reduction, we don’t have a good static analysis tool to calculate independent transitions
- We do now have a version of JPF that groups all transitions between synchronization statements into an atomic block
- Do automatically what we did manually
- Scott Stoller
- Implemented a “Factory” based infrastructure for adding abstractions
- Abstractions play such a key role in model checking that we didn’t want them to struggle with engineering issues instead of creating new abstractions
- We gave them the “point” abstraction of time
- All time-based decisions became nondeterministic
- It is typical to start with the most over-approximated system and use refinement as necessary
- We gave them  the “Universal” planner that can create *all* plans up to a specific size nondeterministically
- Again, common in model checking to use a universal environment

## Model Checking Observations

- Asked never to “run” the code, only model check it
- Keep the results clean from any testing influence
- Performed much better than testing, and, as well as runtime-analysis
- Missed one concurrency error (nobody found this one) and one plan error
- Interesting observations
- Partially 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
- Didn’t use the Universal planner as much as we anticipated
- Rather change the training plans we gave them, probably to be more in control
- Lots of time spent with the heuristic options
- The state space is very large and heuristics were required to look at different parts
- Found a number of bugs in the first version, had a slow 2nd version, and then found all the remaining bugs in the first part of the 3rd version
- Took them some time to get their framework setup, but once done, they were flying
- Had problems with misplaced “atomic” statements
- Would not have happened if these were done automatically
- Found a nasty bug in floating-point arithmetic that slowed them down at the end
- We anticipated a lot more tool errors than actually happened

## Static Analysis Setup

- The experimental conditions for static analysis were different from those for the other tools
- PolySpace Verifier looks for run-time errors, e.g.,
- un-initialized variables/pointers
- out-of-bound array accesses
- overflow/underflow
- The original C++ code was translated into C code instead of Java
- The tool had to be run overnight in a batch mode because of its slow performances
- 4 to 8 hours for the code used in the experiment

## Static Analysis Observations

- A priori static analysis seems easy to use:
- You feed the program to the analyzer, and out comes a list of errors and warnings you can easily sort through
- The experiment shows that it is not that easy:
- Participants didn’t understand how to deal with warnings - there are many more warnings than errors
- It is difficult to understand how approximations in the analysis algorithms impact warnings, unless one has a good understanding of the algorithms

## Static Analysis Observations cont.

- The domain of applicability of each operation flagged as an orange (warning) should be checked in every possible execution context
- There are too many warnings to do this rigorously
- Participants didn’t understand how, and where, to use assertions and stubs to eliminate oranges
- The participants chose to increase the number of execution paths that could be analyzed instead of analyzing the given program
- They tried to make dead code reachable

## Runtime Analysis Setup

- Java PathExplorer
- Required no setup. Instrumentation is automated. No specification or program manipulation is required.
- DBRover
- Rover code was pre-instrumented to emit events of the form (for actions ‘a’ and time points ‘t’):
- start(a,t), success(a,t) and fail(a,t).
- Users had to write a set of temporal formulae for each plan. This was time consuming.

## Java PathExplorerDeadlock and Data race Detection

- Students quickly learned to use tool. Interpretation of results required some training.
- Users found it very easy to apply tool. They applied it instantly when they got a new version of the code, and then with regular intervals.
- Tool found all seeded resource deadlocks and the seeded data race, and quickly. Tool is not designed to find communication deadlocks. Did therefore not find any.
- No false positives or false negatives.
- Extension of tool to handle some communication deadlocks is under way.

## DBRoverTemporal Logic Monitoring

- Students quickly learned to use DBRover. Perhaps because temporal properties followed templates.
- Users found it slightly inconvenient to write specs for new plans. DBRover was therefore only used sporadically.
- Most plan errors (excluding deadlocks and data races) were found by examining printed information. Some were found due to violated temporal properties.
- Automatic generation of specs from plans would have made DBRover a clear success (in the users own words). In particular combined with a universal planner. This work is now being done.

## Testing Observations

- Black box approach. Test cases constructed from the plan specification.
- Maintained a test suite and performed regression testing on each version.
- Looked for concurrency errors and the results of jitter by setting task durations and deadlines to nearly equal values
- Ran software on multiple platforms and modified the task priorities.

## Some Results

- Model
- Checking

- Runtime
- Analysis

- Testing

**Types of Bugs Found in Version 1**

**0**

**2**

**4**

**6**

**8**

**10**

**12**

**14**

**16**

**18**

**Experiment Hour**

- Model
- Checking

- Runtime
- Analysis

- Testing

- Model
- Checking

- Runtime
- Analysis

- Testing

## What we did after the Experiment

## Automated Test Environment for the K9 Rover

**K9**
**executes plan**

**Plan**
** ****Generation**

**Property **
**Generation**

**Trace **
**Analysis**

**Program **
**Instrumentation**

**Simulator**

- trace

- properties

- plan

- plan

**JPF**

## Plan Generation

- class UniversalPlanner { ...
-   static int nNodes = 0;
-   static int tRange = 10;
-   static void Plan(int nn, int tr) {
-     nNodes = nn; tRange = tr;
-     Node plan = UniversalNode();
-     print(plan);
-     assert(false);
-   }
-   static Node UniversalNode() {
-     if(nNodes == 0) return null;
-     if( Verify.randomBool() ) return null;
-     if( Verify.randomBool() )
-       return UniversalTask();
-     return UniversalBlock();
-   }
-   static NodeAttr UniversalNodeAttr() { ... }

- static Node UniversalTask() {
-     NodeAttr na = UniversalNodeAttr();
-     Symbol action = new Symbol();
-     boolean fail = Verify.randomBool();
-     int duration = Verify.random(tRange);
-     Task t = new Task(na, action, fail, duration);
-     nNodes--;
-     return t;
- }
- static Node UniversalBlock() {
-     NodeAttr na = UniversalNodeAttr();
-     nNodes--;
-     ListOfNodes l = new ListOfNodes();
-     for(Node n=UniversalNode();n!=null;n=UniversalNode())
- 	l.addNode(n);
-     Block b = new Block(na,l);
-     return b;
- }

## Plan Properties

- ◊ start(plan)
- □ (start(plan) → ◊1,5 start(drive1))
- □ (start(drive1)→( ◊1,30success(drive1)  ◊fail(drive1)))
- □ (success(drive1) → ◊ start(drive2))
- □ (end(drive2) → ◊ success(plan))
- ◊ success(drive1)
- ◊ fail(drive2)

## Enabling Technologies

- Model Checking for test-case generation
- Test-input generation
- Symbolic (execution) model checking
- Test-oracle generation
- From requirements specifications
- Symbolic execution-based Java PathFinder
- Runtime monitoring
- Java PathExplorer

## Model Checking ProgramsNASA’s approach

- Complex programs and rich properties
- Minimalist Approach (*popular abstraction-refinement paradigm is not minimalist)*
- Error-detection
- Change as little as possible from the original and use heuristics
- Use carefully selected abstractions
- It is unclear whether this will scale much beyond 10000 lines of code
- Be even more selective in the parts of the state-space being analyzed – i.e. look only at traces (runtime monitoring)
- Goal: use runtime monitoring in combination with more heavyweight techniques such as model checking
- Apply model checking to reduce overhead of runtime monitoring, i.e. proof certain easy portions of a program correct, and leave the rest for monitoring
- Also, use model checking to generate the test-inputs for runtime monitoring

## Model Checking ProgramsFuture

- ...is very bright
- Since there is an awful lot of problems we have not solved yet
- Word to remember - ***Specialize***
- The problem is too hard to solve for the general case
- too much user assistance required
- Look for light-weight solutions
- E.g. CMC from Stanford – finds errors in protocols by running the protocol (written in C) and extracting the state (and storing it) at predefined points
- For practical success within NASA we’ll need to focus on improving testing, specifically test-case generation
- Distant future – 5-15 years ... or so
- There will not be any *real* low hanging fruit left
- No deadlocks and data races for example
- We’ll need to check rich behavioral properties, specifically how components (including threads/processes) interact
- Challenge for abstraction-centric approaches: Check complex systems with rich properties
- The norm these days are for complex (simple?) systems with simple properties
- Challenge for bug-hunters: “Are you sure you didn’t miss the bug”?

## Backup slides

## Plan Grammar

*Plan          *→ *Node*
*Node        *→  *Block* | *Task*
*Block      *  → (block *NodeAttr*
- 		       :node-list (*NodeList*))
*NodeList*  **→** *Node NodeList* | **
*Task* 	 → (task *NodeAttr*
- 		       :action *Symbol*
- 		      [:fail]
- 		      [:duration *DurationTime*])
*NodeAttr* → :id *Symbol*
- 		      [:start-condition *Condition*]
- 		      [:end-condition *Condition*]
- 		      [:continue-on-failure]
*Condition  *→ (time *StartTime EndTime*)

## The Increased need forSoftware within NASA

**The Increased need for****Software within NASA**

- Systems must support **remote exploration**
- Systems must be **more autonomous**
- Systems must do **more complex tasks**

***When people think of space, they think of rocket plumes and the Space Shuttle, but the future of space is information technology...***
**Daniel S. Goldin, **
**Previous NASA Administrator**

## Java Program with Resource Deadlock

- T1:
- synchronized(**R1**){
-   ..
-   synchronized(**R2**){..}
-   ..
- }

- T2:
- synchronized(**R2**){
-   ..
-   synchronized(**R1**){..}
-   ..
- }

**Deadlock**: if T1 takes R1 and then T2 takes R2

## Data Races

- A datarace can occur between a set of 2 threads T={T1,T2} if they access a shared variable V and there is a state of the execution where T1 can write to the variable and T2 can write to or read from the variable without using a _shared _lock.

- T1

- T2

- V

## Java Program with Data Race

**Data race**: if T1 reads sum and then T2 reads sum
- where after the additions are made. Result is +100 or
- +50, depending on who writes first, not +150