# Presentation: 502670

## Integrating Model Checking and Procedural Languages (FI03) 

**Tim Menzies**
- West Virginia University_[tim@menzies.us](mailto:tim@menzies.us)_

**David Owen**
- West Virginia University
- _[drobo75@hotmail.com](mailto:drobo75@hotmail.com)__  _

## Model-based tools (MATLAB) for NASA projects

**GLAST=**
**“****gamma ray large area space  telescope”**
****** ****studies high-energy objects**

**STEREO= ****“solar terrestrial relations observatory”**
****** ****studies 3D structure of coronal mass ejections**

## Coming soon to softwarenear you: model-baseddevelopment

**           ****Rhapsody from I-Logix**
**Rose Real-Time from Rational**
**                                       ****Esterel                                 ****             Simulink/ Stateflow **
**                   ****Stanley/ Livingston**
**But checking these is hard**
- No longer  testing procedural software
- Test “properties”, not “structure”
**Issues:**
- Hard when nondeterministic
- Checking properties on all pathways= HARD (NP-hard; i.e. O(2N)
**When complete search is too slow**
- Will stochastic search do?

##  Model-Based Development

## Why model-based development?

**Source: Esterel Technologies**

- - 37.5 %

- - 25 %

- - 75 %

- - 50 %

## Costs: write, run, rewrite

*most 2 times  between Q and R:*
*   **[]((Q & <>R) -> *
*       **((!P & !R) U (R | ((P & !R) U **           (R | ((!P & !R) U (R | ((P & !R)**               U  (R | (!P U R))))))))))*

**Costs: write, run, rewrite**

**Write**
- System model
- Mathematical abstraction of program
- Properties model
- Temporal logic description of key requirements
- Negate, search for counter-examples
- PhD-level mathematical expertise
**Run**
- Explore all pathways
- Exponential time
**Rewrite**
- Theory too big
- Use some abstraction to shrink theory

## Random vs complete search

**Animation by Bart Selman**

_**Source:**_
**IJCAI-01 tutorial**
**Gomes, Hogg, **
**Walsh, Zhang**

## LURCH: random search of nondeterministic FSM as NAYOs

**LURCH: random search ****of nondeterministic FSM as NAYOs**

- FSM

- NAYO graph = <V+,E+>
- V= and | or;
- E= yes  | no
- for (each FSM ***f***)     for (each state)
-           make an OR-node;           draw NO-edges to all other states in ***f ***;
-      for (each transition)
-           make an AND-node ***a***;
-           draw YES-edges:               from ***current ***(state) to ***a***, from inputs to ***a***,
-                from ***a ***to outputs, and from ***a ***to ***next ***(state);

**B2**

## LURCH and “C”

**int x_turn() {**
**	****if (t != X) return FALSE;**
**	****t = UNDEF; return TRUE;**
**}**
**int o_turn() {**
**	****if (t != O) return FALSE;**
**	****t = UNDEF; return TRUE;**
**}**

**%%**
**s1_1-blank; (x_turn()); {t = O;}; s1_1-X;**
**s1_1-blank; (o_turn()); {t = X;}; s1_1-O; **
**s1_2-X;**
**s1_2-blank; (x_turn()); {t = O;}; s1_2-X;**
**s1_2-blank; (o_turn()); {t = X;}; s1_2-O;**
**s2_1-blank; (x_turn()); {t = O;}; s2_1-X;**
**s2_1-blank; (o_turn()); {t = X;}; s2_1-O;**
**s2_2-O;**
**s2_2-blank; (x_turn()); {t = O;}; s2_2-X;**
**s2_2-blank; (o_turn()); {t = X;}; s2_2-O;**

**no-win; s1_1-X,s1_2-X; -; win;**
**no-win; s2_1-X,s2_2-X; -; win;**
**no-win; s1_1-X,s2_1-X; -; win;**
**no-win; s1_2-X,s2_2-X; -; win;**
**no-win; s1_1-X,s2_2-X; -; win;**
**no-win; s1_2-X,s2_1-X; -; win;**
**no-win; s1_1-O,s1_2-O; -; win;**
**no-win; s2_1-O,s2_2-O; -; win;**
**no-win; s1_1-O,s2_1-O; -; win;**
**no-win; s1_2-O,s2_2-O; -; win;**
**no-win; s1_1-O,s2_2-O; -; win;**
**no-win; s1_2-O,s2_1-O; -; win;**

**LURCH ****and “C”**

##  NAYO search = NP-hard

** ****NAYO search = NP-hard**

- This NAYO represents the SAT query

- NAYO Search **∈** NP

- A solution—a DAG ofYES-edges connectingonly compatible (no NO-edges) nodes—can beverified in polynomial time.

## Since NP-hard, try stochastic

**Machines with local states**
- Machines= variables with N possible assignments
**Global state: **
- an assignment to all variables
**“****Global state path”:**
-  list of global states
- path[i] “earlier” than path[j] i < j.

**“****Thrash”**
- Explore transitions in random order
**“****Frontier”: **
- Reachable local states that contradict local states found earlier
- Asychronous mode: “next” when |fronter|=1
- Synchronous model: “next” when no new local states found
**Inputs to path[i]  are**
- FIRST: frontier [i -1]
- THEN :reached[i -1]
- minus local states that contradict frontier

## “Looping” and “Saturation”

**Inter- iteration: **
- global state hashes in any iteration
- accumulates over many iterations
- Used to detect “saturation”
**LURCH stops on “saturation”**
- stop if less than X% new global states seen in this iteration
**lurch –p 0.05**

**“****Looping” and “Saturation”**

**LURCH “iterates”**
- One iteration=  one global state path
- Default # of iterations: 500
**lurch –I 500**
**Internally:**
- each global state hashed to a 32-bit int
**Intra- iteration: **
- keeps hashes found in this iteration
- cleared after each iteration
**“****Collision”: **
- same global state reached again
- checked against inter-iteration memory
**“****Loop”:**
- Too many collisions
- max collisions default = 10
**lurch –c 10**

## Some LURCHresults

- spin

- lurch

**dining philosophers**

- spin

- lurch

**nqueens n=: 4..14**

## Flight Guidance System:

**Runtime (secs)**

** ****Usually, finds what SMV finds**
** ****Often, much faster**
** ****Often, uses less memory **
** ****Sometimes, (8/40) random search failed**
** ****Further work: tunings; larger sample size**

**memory (MB)**

**Flight Guidance System:**
- RSML*-e* model from Rockwell Collins Inc.
- Pitch and Roll commands, complex mode logic
**Convert  to LURCH,SMV**
- Find errors in using historical records that SMV would detect
- Compare SMV, LURCH

**Mats Heimdahl***UMN*

- Jimin Ga *UMN*

## When 100% assurance is essential
When other, more complete methods, work
But if the choice is LURCH vs “nothing at all”
Considering LURCH-ing

**When other, more complete methods, work**
**But if the choice is LURCH vs “nothing at all”**
- Considering LURCH-ing

**When not to LURCH**

## Linking LURCH to procedures (method #1: spiderweb)

**Tiny formal model for the interfaces**
**Large procedural systems (in “C”)**
**Execution= traversal FSMs**
- Call “C” functions as transition side-effects
**Advantage:**
- Usability: most NASA programmers code in “C” (or ADA)

## Linking LURCH to procedures (method #2: MATLAB)

**enum { UNDEF, X, O } turn = X;**
**int x_turn() {**
**	****if (t != X) return FALSE;**
**	****t = UNDEF; return TRUE;}**
**int o_turn() {**
**	****if (t != O) return FALSE;**
**	****t = UNDEF; return TRUE;}**

**%%**
**s1_1-blank; (x_turn()); {t = O;}; s1_1-X;**
**s1_1-blank; (o_turn()); {t = X;}; s1_1-O; **
**s1_2-X;**
**s1_2-blank; (x_turn()); {t = O;}; s1_2-X;**
**s1_2-blank; (o_turn()); {t = X;}; s1_2-O;**
**s2_1-blank; (x_turn()); {t = O;}; s2_1-X;**
**s2_1-blank; (o_turn()); {t = X;}; s2_1-O;**
**s2_2-O;**
**s2_2-blank; (x_turn()); {t = O;}; s2_2-X;**
**s2_2-blank; (o_turn()); {t = X;}; s2_2-O;**

## Linking LURCH to procedures (method #3: JPF)

**NASA’s engineering for complex systems**
**JAVA pathfinder**
- Runtime monitoring of JAVA
- Or C++ translated to JAVA (automatically)
**Used for (e.g.) test case generation ****or detection of livelocks**

- Is LURCH a better search strategy than
- depth first search?

- C++

## Questions? Comments?

** **