# Presentation: 571936

## Towards a Compositional SPIN

- Corina Păsăreanu
*QSS, NASA Ames Research Center*
- Dimitra Giannakopoulou
*RIACS/USRA, NASA Ames Research Center*

## Main objective:
An integrated environment that supports software development and verification/validation throughout the lifecycle; detect integration problems early, prior to coding
Approach: 
Compositional (“divide and conquer”) verification, for increased scalability, at design level
Use design level artifacts to improve/aid coding, testing and fault containment

- An integrated environment that supports software development and verification/validation throughout the lifecycle; detect** ***integration *problems early, prior to coding
**Approach: **
- Compositional (“divide and conquer”) verification, for increased scalability, at design level
- Use design level artifacts to improve/aid coding, testing and fault containment

- Compositional
- Verification

- Testing

- Design

- Coding

- Requirements

- Deployment

- implementations

- Project Overview

## Towards a Compositional SPIN

- Learning based compositional analysis for increased scalability [TACAS’03] – LTSA tool
- Contributions
- Generic tool architecture for learning based assume guarantee reasoning
- Handles multiple components
- Uses SPIN to answer model checking questions
- Other tools can be used (e.g. Java PathFinder)
- Heuristic for automated generation of interface specifications
- Application to realistic resource arbiter for a spacecraft
- Significant memory gains over “traditional” non-compositional model checking

## Outline

- Introduction
- Background: assume-guarantee reasoning and learning
- Tool architecture
- Implementation
- Using SPIN for answering learning questions
- Promela subset
- Case study: MER Arbiter model
- Description, results, discussion
- Conclusions and future work

## Compositional Verification

- M2

- M1

- A

- Check P on entire system: too many states!
- Use the natural decomposition of the system into its components to break-up the verification task
- Check components in isolation:
- 	Does M1 satisfy P?
- Typically a component is designed to satisfy its requirements in *specific* contexts / environments
- Assume-guarantee reasoning: introduces assumption A representing M1’s “context”

- Does system made up of M1 and M2 satisfy property P?

**Notes:**
Compositional verification presents a promising way of dealing with the verification of large systems. It is a “divide and conquer” approach: 
the property of a system is decomposed into properties of its components, which are then checked separately. For example
let us assume we want to check that a system composed of components M1 and M2, and after decomposing its properties, we need to check
that component M1 satisfies P. However, more often than not, verification of a component in isolation is not very meaningful, because the component is designed to satisfy its requirements in a specific context, or environment. Assume-guarantee reasoning addresses this issue by introducing assumptions, that encode or characterize as
abstractly as possible, the expected behavior of the component environment, at the level of its interactions with the component. 

The simplest assume-guarantee rule which we have found useful when checking safety properties is the following, where we use here the standard notation for such rules:
under an assumption A, does the component satisfy the property? To complete the proof, it is of course necessary to then “discharge” the assumption, i.e. show that the actual environment indeed behaves as described. 

## Assume-Guarantee Rules

- M2

- M1

- A

- Simplest assume-guarantee rule
- We can also handle symmetric rules

- How do we come up with the assumption?
- (usually a difficult manual process)

- Reason about triples:
- A M P
- The formula is *true* if whenever M is part of a system that satisfies A, then the system must also guarantee P

**Notes:**
Compositional verification presents a promising way of dealing with the verification of large systems. It is a “divide and conquer” approach: 
the property of a system is decomposed into properties of its components, which are then checked separately. For example
let us assume we want to check that a system composed of components M1 and M2, and after decomposing its properties, we need to check
that component M1 satisfies P. However, more often than not, verification of a component in isolation is not very meaningful, because the component is designed to satisfy its requirements in a specific context, or environment. Assume-guarantee reasoning addresses this issue by introducing assumptions, that encode or characterize as
abstractly as possible, the expected behavior of the component environment, at the level of its interactions with the component. 

The simplest assume-guarantee rule which we have found useful when checking safety properties is the following, where we use here the standard notation for such rules:
under an assumption A, does the component satisfy the property? To complete the proof, it is of course necessary to then “discharge” the assumption, i.e. show that the actual environment indeed behaves as described. 

## Approaches

- Infer assumptions automatically
- Two solutions developed
- Algorithmic generation of assumption (controller); knowledge of environment **is not** required [ASE’02]
- I**ncremental** assumption computation based on counterexamples, learning and knowledge of environment [TACAS’03, SAVCBS’03 (symmetric rules)]

**Notes:**
The first solution, that will be presented in the first part of this talk, is an algorithmic, non-incremental, generation of assumptions. The drawback is that if the computation runs out of memory, i.e. if component state space is too large, no assumption will be obtained as a result. The advantage is that it does not require knowledge of the environment.

The second, is an incremental approach, based on counterexamples and learning. Sounds mysterious but we hope to make it simple and clear after our presentation. Advantage: is an any-time approach, which means that it produces a finite sequence of approximations to an assumption that can be used to obtain conclusive results in assume-guarantee reasoning. If it runs out of memory, intermediate assumptions can still be useful.  However, it requires knowledge of the environment. 

## Formalisms

- Components modeled as finite state machines (FSM)
- FSMs assembled with parallel composition operator “||”
- Synchronizes shared actions, interleaves remaining actions
- A property P is a FSM
- P describes all legal behaviors
- P**err** *–* determinize & complete P; bad behaviors lead to “**error**”
- Component M satisfies P iff error state unreachable in (M || P**err**)
- Assume-guarantee reasoning
- Assumptions and guarantees are FSMs
- A M P holds iff error state unreachable in (A || M || P**err**)
- The alphabet of A, A, contains all environment actions that appear in P

## Example 

- Example

**Input**

** ****in**

**send**

**ack**

**Output**

** ****out**

**send**

**ack**

**Order****err**

** ****in**

** ****out**

** ****in**

** ****out**

**||**

**Notes:**
Communication channel consisting of an input and an output component; Grey states are initial states. Highlighted actions are common to their alphabets and will be synchronized when the processes are composed.
property: inputs and outputs come in matched pairs; input always preceding output. Error state is red state.

## Computing the Weakest Assumption

- Given component *M*, property *P*, and the interface of *M *with its environment, generate the weakest environment assumption *A* such that: assuming *A*, *M* ╞ *P*
- Weakest means that for all environments *E*:* *
- (*E* || *M* ╞  *P*)  **IFF**  *E*╞ *A*

**Notes:**
weakest means that it restricts the environment no more and no less than it needs to

## Learning for Assume-guarantee Reasoning

- Use an off-the-shelf learning algorithm to build appropriate assumption for the rule
- Process is *iterative*
- Assumptions are generated by querying the system, and are gradually refined
- Queries are answered by model checking
- Refinement is based on counterexamples obtained by model checking
- Termination is guaranteed
- Extended with symmetric rules

**Notes:**
The aim is to construct an assumption that makes the assume guarantee rule return conclusive results, i.e. a yes or a no. 
We provide a framework that performs assume-guarantee reasoning in an incremental and fully automated way; uses learning and MC.
Learning is used to build an initial approximate assumption based on some knowledge about component M1
MC is then used to see if this assumption is good enough for checking the rest of the property using the assume-guarantee rule.
 We first check if the first step of the rule holds (remember we use LTSA so we are talking about LTSs)
If this is not the case, it means the assumption is too weak so it does not prevent M1 from getting to the error sate.
... strengthen assumption to eliminate the counterexample
If the first step holds, we then try to discharge ... done
Otherwise, further analysis is needed to determine the cause of the error.
If this is a real error, we are done.
Otherwise, it is a spurious error due to the fact that although the assumption is strong enough to prevent M1 from getting to the error, it is actually too strong, and it has to be weakened (add more behaviors).
... repeat

*guaranteed to terminate* will maybe become clear why when we describe the characteristics of the learning, but more in the paper 

## Learning with L*

- L* algorithm by Angluin, improved by Rivest & Schapire
- Learns an unknown regular language U (over alphabet ) and produces a DFA A such that  L(A) = U
- Uses a teacher to answer two types of questions

- L*

- conjecture: Ai

- query: string s

- true

- false

- remove string t

- add string t

- output DFA A
- such that L(A) = U

- true

- false

- false

- is s in U?

- is L(Ai)=U?

**Notes:**
# queries: (kn2 + n logm) 
-> m is size of largest counterexample, k is size of alphabet
maintains a table that records whether strings in  belong to U

## Learning Assumptions

- Use L* to generate candidate assumptions
- A = (M1  P)  M2

- L*

- query: string s

- true

- false

- conjecture: Ai

- true

- false

- true

- yes

- false

- no

- remove counterex.

- add counterex.

- P holds in
- M1 || M2

- P violated

-    A      M1 	    P
- *true*     M2 	   A
- *true* M1 || M2  P

**Model Checking**

**Notes:**
# queries: (kn2 + n logm) 
-> m is size of largest counterexample, k is size of alphabet
maintains a table that records whether strings in  belong to U

## Characteristics

- Terminates with *minimal *automaton A for  U
- Generates DFA candidates Ai: |A1| < | A2| < ... < |A|
- Produces at most n candidates, where n = |A|
- # queries: (kn2 + n logm),
- m is size of largest counterexample, k is size of alphabet

- For n components (M1 || M2 || ... || Mn) apply algorithm recursively:
- Ai M1 P as before
- *true* M2 || ... || MnAi invokes the framework

## Learning Interface Specifications

- *true* P Ai

- Compute an assumption (as weak as possible) for a component M1 to guarantee some property P, when environment is not available
- A = P

- L*

**conjecture:** Ai

- Ai M1 P

**true**

**counterexample**

**true**

**false**

**return A****i**

**counterexample**

- not accurate with respect
- to !P || !M1

## Implementation in SPIN

- Stand-alone application
- Invokes SPIN for queries and conjectures
- Handles only a Promela subset
- Components are processes
- Communication through rendezvous channels
- Safety properties
- SPIN trace assertions
- Checking assume-guarantee triples
- Encode assumptions into environment processes that run in parallel with components

## Case Study

- Model derived from MER Resource Arbiter
- Local management of resource contention between resource consumers (e.g. science instruments, communication systems)
- Avoid simultaneous conflicts (e.g. driving while capturing a camera image are mutually incompatible)
- Enforce orderly activity in accordance with predefined priorities encoded in a lookup table
- 5 resources
- Comm, Drive, PanCam, Arm, Rat
- 5 User threads
- Non-deterministically decide to use any of the 5 resources
- ~3000 LOC
- Checked several safety properties

## Arbiter Architecture

**Property P**
- Mutual exclusion between resources
- Comm and Drive can not be used at the same time

## MER Arbiter Property

**Mutual exclusion between resources**
- Comm and Drive can not be used at the same time
- PanCam and Arm can not be used at the same time
- Rat and Arm can not be used at the same time

## Incremental Property Checking

- Compute A1 ... A5 s.t.
- A1 U1 P
- A2 U2 A1
- A3 U3 A2
- A4 U4 A3
- A5 U5 A4
- true ARB A5
- Result
**P holds on U****1**** || .. || U****5**** || ARB**
- Two techniques
- Recursive invocation
- Interface specification
- Comparison with non-compositional analysis

## Analysis Results

| Analysis | Memory | State Space | Time
tmodel    tcompile   trun | Assumption Size |
| --- | --- | --- | --- | --- |
| Monolithic | 544 MB | 3.9e+06 | 0.02s    0.8s   33.7s | N/A |
| Recursive | 2.6 MB | 1002 | 0.03s    1.1s   0.03s | 6 .. 12 |
| Interface | 2.6 MB | 2941 | 0.04s    1.3s   0.02s | 12 |

- Results do not reflect the cost of generating the assumptions

## Cost of Assumption Generation

| Analysis | queries | oracle1 | oracle2 | tSPIN+tLearn | MemLearn | tLTSA | MemLTSA |
| --- | --- | --- | --- | --- | --- | --- | --- |
| Recursive | 4884 | 48 | 1 | 5646.3s | 1743K | 42.8s | 20400K |
| Interface
(A1) | 852 | 12 | 1 | 818.2s | 508K | 3.07s | 4845K |

**LTSA tool**

## Discussion

- Significant memory savings
- Serious time overhead
- Experimented with SPIN’s feature for separate compilation
- Encode assumptions as never claims
- Restrict search of the verifier
- New encoding for queries
- Significant improvement
- Cost of interface generation reduced from 818.213s to 185.185s

## Conclusion and Future Work

- Tool architecture for compositional verification
- Uses L* for automatic derivation of assumptions
- Automated derivation of interface specification
- “Loose” integration with SPIN
- Model checking for queries and conjectures
- Application to Arbiter case study
- Significant memory gains
- Serious time overhead ; techniques to address this issue
- Future work
- Tighter integration with SPIN
- Parallel checks for queries
- Investigate buffered message passing communication
- Liveness (learning for infinitary regular sets)
- Distinguish between read and write operations