# Presentation: 045464

## Automated Model Revision:Moving Beyond Model Checking

*Borzoo Bonakdarpour*
*Sandeep S. Kulkarni*

- The Sixth NASA Langley Formal Methods Workshop

## The Notion of Program Revision

_*Question*_:
- Is it possible to *revise* the program automatically such that it satisfies the failed property (due to *change of environment* or *incomplete specification*) while preserving existing properties?

- Counterexample

- Property

- Model
- Checker

- Program

- The Sixth NASA Langley Formal Methods Workshop

**Notes:**
1	2:3.j

## Our Criteria in This Research

- We focus on *interesting** **properties* (e.g., UNITY) that are typically used in specifying systems
- We consider *real-time*, *centralized*, and *distributed* programs
- We consider:
*Closed* systems, where programs do not interact with the environment
*Open* systems, where programs interact with the environment
- Identifying cases where revising existing programs is *feasible* in terms of time and space

- The Sixth NASA Langley Formal Methods Workshop

## Outline

- Adding fault-tolerance to real-time programs
- Automated addition of UNITY properties
- Adding fault-tolerance to distributed programs
- Conclusion and future work

- The Sixth NASA Langley Formal Methods Workshop

## Real-Time Centralized Systems

- The Sixth NASA Langley Formal Methods Workshop

## Traffic Controller

- A one-lane bridge is controlled by two traffic signals at the two ends of the bridge.

- (*sig*1 = G)   (1 ≤ *x*1 ≤ 10)  	 	*sig*1 := Y;
- []

- (1)

- (2)

- (*sig*1 = Y)   (1 ≤ *y*1 ≤ 2)  		*sig**i* := R ;
- []

- (*sig*2 = R)   (*z*1 ≤ 1)  		*sig*2 := G ;
- []

_***Specification***_***:***** **{(*s*0, *s*1) |  *sig*1 (*s*1) ≠ R        *sig*2 (*s*1) ≠ R}

_***Program actions:***_

- ((*sig*1 = G)   (*x*1 ≤ 10)) 
- ((*sig*1 = Y )  (*y*1 ≤ 2))     
- ((*sig*1 = R)   (*z*2 ≤ 1))  		**wait**;

- The Sixth NASA Langley Formal Methods Workshop

## Traffic Controller (cont’d)

_***Fault action:***__*** ***_

- (1)

- (2)

- (*z*1 ≤ 1)    (*z*2 > 1)
- (*z*1 ≤ 1)    (*z*2 = 0)
*sig*1 = G
*sig*2 = G

- The Sixth NASA Langley Formal Methods Workshop

## Problem Statement

***Invariant***

***f***

***f***

***f***

***Fault-Span***

***State space***

*p*

*p*

*p*

***p***

***p***

***p***

*p*

*p*

*p*

*p*

***f***

***f***

- The Sixth NASA Langley Formal Methods Workshop

## Traffic Controller (cont’d)

- (*sig*1 = *G*)   (1 ≤ *x*1 ≤ 10)	  	 			*sig*1 := *Y*;
- []

- (*sig*1 = *Y*)   (1 ≤ *y*1 ≤ 2)	  				*sig**i* := *R* ;
- []

- (*sig*2 = *R*)   (*z*1 ≤ 1)  (*sig*1 = *R*) 				*sig*2 := *G* ;
- []

_***Fault-Tolerant Program actions:***_

- ((*sig*1 = *G*)   (*x*1 ≤ 1.j)) 
- ((*sig*1 = Y )  (*y*1 ≤ 2))    ((*sig*1 = *R*)   (*z*2 ≤ 1))  		**wait**;
- []
- (*sig*1 ≠ *R*  *sig*2 ≠ R)  (*z*1, *z*2 ≤ 1) 				*sig*1, *sig*2 := *R*;
- []
- (*sig*1 = *sig*2 = *R*)  (*z*1, z2 ≤ 4)  (*t*1 ≤ 3)				**wait**;
- []
- (*sig*1 = *sig*2 = *R*)  (*z*1, *z*2 > 1)					**skip**;
- []
- (*sig*1 = *sig*2 = *R*)  (*z*1, *z*2 > 1)   (*t*2 ≤ 7) 			**wait**;

- The Sixth NASA Langley Formal Methods Workshop

## Summary of Results

|  | Safety | Timing Constraints | Recovery | One Bounded Response | Multiple Bounded Response |
| --- | --- | --- | --- | --- | --- |
| Soft-failsafe |  |  |  | Polynomial time, sound, and complete algorithm |  |
| Hard-failsafe |  |  |  |  | Open problem |
| Nonmasking |  |  |  |  |  |
| Soft-masking |  |  |  |  |  |
| Hard-masking |  |  |  | NP-complete | NP-complete |

- The Sixth NASA Langley Formal Methods Workshop

## Untimed Centralized Systems

- The Sixth NASA Langley Formal Methods Workshop

## Revising Programs wrt.UNITY Properties

*P ****leads-to****** ****Q*:
- □( *P * ◊*Q *)

***P***

***Q***

- The Sixth NASA Langley Formal Methods Workshop

## Revising Programs wrt.UNITY Properties (cont’d)

*P*

*Q*

**Case 1: *****Deadlock states***

*s*0

*s*1

*s*2

*S**p*

**Revising Programs wrt.****UNITY Properties (cont’d)**

- Remove transitions (*s*1, *s*2)  if *s*2  *P* and *Q* is not reachable from *s*2

- The Sixth NASA Langley Formal Methods Workshop

## Revising Programs wrt.UNITY Properties (cont’d)

*P*

*Q*

- Break cycles reachable from *P**.*

*s*1

*s*4

*s*2

*s*3

**Case 2: *****Cycles***

*s*0

*S**p*

**Revising Programs wrt.****UNITY Properties (cont’d)**

- The Sixth NASA Langley Formal Methods Workshop

## Revising Programs wrt.UNITY Properties (cont’d)

| Property | Complexity (state space) |
| --- | --- |
| Leads-To
 (P  Q) | Polynomial time,
sound, and complete algorithm  |
| Leads-To 
(with maximum non-determinism) | NP-complete |
| Double Leads-To 
 (true   Q)   (true   T) | NP-complete |

**Revising Programs wrt.****UNITY Properties (cont’d)**

- The Sixth NASA Langley Formal Methods Workshop

## Untimed Distributed Systems

- The Sixth NASA Langley Formal Methods Workshop

## Adding Fault-Tolerance

**Adding Fault-Tolerance**

_*Decision*_ *d.g*  {0, 1}

- (*d.j* = )    ( *f.j* = *false*)		*d.j* := *d.g*
- (*d.j*  )    ( *f.j* = *false*)		*f.j* := *true*

***GENERAL***

***NON-GENERALS***

_*Program actions*__*:*_

- The Sixth NASA Langley Formal Methods Workshop

## Adding Fault-Tolerance (cont’d)

_*Byzantine?*_
*b.g*  {*false*, *true*}

- (*b.j ,* *b.k* , *b.l , b.g *= *false*)		*b.j* := *true*
- (*b.j* := *true*) 			*d.j* := 0|1

_*Fault actions*__*:*_

- The Sixth NASA Langley Formal Methods Workshop

## Safety specification:
Agreement: The final decision of any two non-Byzantine processes cannot be different.

Validity: If the general is non-Byzantine then the final decision of a non-Byzantine process must be the same as that of the general.

Fact:
The program does not meet the safety specification in the presence of faults:

d.g = 1,   b.g = false
d.k = 1,   f.k = true
d.g = 0,   b.g = true
d.j = 0,    f.j = true

*Agreement:* The final decision of any two non-Byzantine processes cannot be different.
*Validity:* If the general is non-Byzantine then the final decision of a non-Byzantine process must be the same as that of the general.
_*Fact*_*:*
- The program does not meet the safety specification in the presence of faults:
*d.g* = 1,   *b.g* = *false*
*d.k* = 1,*   f.k* = *true*
*d.g* = 0,   *b.g* = *true*
*d.j* = 0,    *f.j* = *true*

**Adding Fault-Tolerance (cont’d)**

- The Sixth NASA Langley Formal Methods Workshop

## The Synthesized Program by the Tool SYCRAFT

- -----------------------------------------------------------------------------------------------------
- UNCHANGED ACTIONS:
- -----------------------------------------------------------------------------------------------------
- 1- (d.j==2) & !(f.j==1) & !(b.j==1) 		 (d.j:=dg)
- -----------------------------------------------------------------------------------------------------
- REVISED ACTIONS:
- -----------------------------------------------------------------------------------------------------
- 2- (b.j==0) & (d.j==1) & (d.k==1) & (f.j==0) 	 	(f.j:=1)
- 3- (b.j==0) & (d.j==0) & (d.l==0) & (f.j==0) 		(f.j:=1)
- 4- (b.j==0) & (d.j==0) & (d.k==0) & (f.j==0) 		(f.j:=1)
- 5- (b.j==0) & (d.j==1) & (d.l==1) & (f.j==0) 	 	(f.j:=1)
- -----------------------------------------------------------------------------------------------------
- NEW RECOVERY ACTIONS:
- -----------------------------------------------------------------------------------------------------
- 6- (b.j==0) & (d.j==0) & (d.l==1) & (d.k==1) & (f.j==0)    (d.j:=1)
- 7- (b.j==0) & (d.j==1) & (d.l==0) & (d.k==0) & (f.j==0)    (d.j:=0)
- 8- (b.j==0) & (d.j==0) & (d.l==1) & (d.k==1) & (f.j==0)    (d.j:=1), (f.j:=1)
- 9- (b.j==0) & (d.j==1) & (d.l==0) & (d.k==0) & (f.j==0)    (d.j:=0), (f.j:=1)
- -----------------------------------------------------------------------------------------------------

- The Sixth NASA Langley Formal Methods Workshop

## Experimental Results

_*Implementation of the heuristics:*_
- C++
- CuDD (Colorado University Decision Diagram Package)
- The tool ***SYCRAFT******  ***(http://www.cse.msu.edu/~borzoo/sycraft)
_*Experiments:*_
- Sun Fire V40z,
- with 4x dual-core Opteron processors, and
- 16 GB RAM

- The Sixth NASA Langley Formal Methods Workshop

## Experimental Results – Time

*Total Synthesis* Time
- vs.
- Number of Processes

*Deadlock Resolution* Time
- vs.
- Number of Processes

- The Sixth NASA Langley Formal Methods Workshop

## Experimental Results – Memory

*Memory* (KB)
- vs.
- State Space

- The Sixth NASA Langley Formal Methods Workshop

## Future Work

- Applying *model checking techniques* in the context of synthesis
- Abstraction-refinement
- SMT/QBF-based
- Distributed/parallel
- Synthesizing *multi-tolerant* real-time programs
- Adding fault-tolerance to *hybrid systems*
- Synthesizing programs with multiple concerns (e.g., security, communication, real-time, fault-tolerance) using *epistemic logic*
- Program synthesis using *graph mining* and *machine learning* techniques

- The Sixth NASA Langley Formal Methods Workshop

**Notes:**
2	1.j:3.j
Path -> why?
Long-Term goal in embedded system -> hybrid systems

## Thank You!

- The Sixth NASA Langley Formal Methods Workshop