Part 1: Specifying and Verifying Transition Systems in NuSMV

Notes based on the course on Model Checking by Prof. B. Srivathsan (CMI). Lecture Video

1. Introduction to NuSMV Transition Systems

NuSMV is a symbolic model checker used to describe and verify finite state transition systems.

A transition system in NuSMV is specified by defining:

  1. The states (variables and their domains)
  2. The initial states
  3. The transition relations (how the system moves from one state to another)

2. Basic Transition System Example

Scenario: A simple system with two states l1 and l2. The initial state is l1, and transitions go from l1 to l2 and back from l2 to l1.

Example 
MODULE main
VAR
  location : {l1, l2};

ASSIGN
  init(location) := l1;
  next(location) := case
    location = l1 : l2;
    location = l2 : l1;
  esac;

3. Running NuSMV Commands

Assuming the above code is saved in a file named intro_demo.smv, follow these steps in the terminal:

NuSMV -int

This starts NuSMV in interactive mode. Within NuSMV, enter:

read_model -i intro_demo.smv
flatten_hierarchy
encode_variables
build_model

Alternatively, do NuSMV -int intro_demo.smv, then go.

4. Exploring the Model

5. Extended Example: Program Graph with Variable

Now, consider a system with: States l1 and l2. An integer variable x ranging from 0 to 100. Transition from l1 to l2 allowed only if x < 10. When moving from l2 to l1, x increments by 1 (bounded by 100). NuSMV supports only bounded variables.

Example 
MODULE main
VAR
  location : {l1, l2};
  x : 0..100;

ASSIGN
  init(location) := l1;
  init(x) := 0;

  next(location) := case
    (location = l1) & (x < 10) : l2;
    (location = l2) : l1;
    TRUE : location;  # Default: don't change location
  esac;

  next(x) := case
    (location = l1) : x;
    (location = l2) & (x < 100) : x + 1;
    TRUE : x;
  esac;

6. Running and Simulating the Extended Model

To exit the current session use the command quit

Load and build the model as before:

read_model -i pg_demo.smv
flatten_hierarchy
encode_variables
build_model

or

NuSMV -int pg_demo.smv
go

Check the initial state:

7. Model with Boolean and Enum Variables

Example with: Boolean variable request, Enum variable status is either ready or busy

Example 
MODULE main
VAR
  request : boolean;
  status : {ready, busy};

ASSIGN
  init(status) := ready;

  next(status) := case
    request : busy;
    TRUE : {ready, busy};
  esac;

8. Exploring and Simulating

Loading and build:

NuSMV -int request_busy_demo.smv
go

9. Specifying and Checking Requirements

Example Execution 1:

Example 1

Example Execution 2:

Example 2

A transition system satisfies a requirement if all its executions satisfy the requirement.

NuSMV supports temporal logic specifications, especially LTL (Linear Temporal Logic), to verify properties such as:

Example 1: Check if x >= 0 always holds in pg_demo.smv

NuSMV -int pg_demo.smv
go
check_ltlspec -p "G (x >= 0)"

NuSMV output will confirm whether the specification is true.

Example 2: Check if request = FALSE always holds in request_busy_demo.smv

NuSMV -int request_busy_demo.smv
go
check_ltlspec -p "G (request = FALSE)"

F(request=1) is false in EE 2 because of the third execution.

NuSMV will state that the specification is false and provide a counterexample execution.

Example 3: Check if eventually x >= 5 holds in pg_demo.smv (see Example Execution 1).

NuSMV -int pg_demo.smv
go
check_ltlspec -p "F (x >= 5)"

Expected output: Specification F x >= 5 is true

Combining G and F

Example 4: Check if whenever request is true, status eventually becomes busy in request_busy_demo.smv

NuSMV -int request_busy_demo.smv
go
check_ltlspec -p "G (request = TRUE -> F (status = busy))"

NuSMV should confirm this property is true. This is not easy to check by just looking at the transition system.

10. Summary

This lecture prepares you to model systems and formally verify their properties using NuSMV.

Part 2: Modeling Hardware Circuits in NuSMV

Introduction

In this lecture, we explore how to describe hardware circuits using the NuSMV tool. Building on prior knowledge of modeling simple transition systems, we delve into three parts:

  1. Modeling a simple circuit.
  2. Exploring more complex circuits like NAND gates.
  3. Using hierarchical designs and modules, culminating in a 3-bit counter example.

1. Simple Circuit Modeling

Circuit Description

Example 
MODULE main
VAR
  x : boolean;
  r : boolean;

DEFINE
  y := !(x xor r);

ASSIGN
  init(r) := FALSE;
  next(r) := x xor r;

Key Modeling Details in NuSMV

Simulation and Reachable States

Important Notes

Use of DEFINE is crucial for outputs depending on current state without delay. State space is determined solely by variables in VAR.

2. NAND Gate Examples

alt text

Example 
MODULE main
VAR
  in1 : boolean;
  in2 : boolean;

DEFINE
  out := !(in1 & in2);

NAND Gate With Zero Delay Inputs: in1, in2 (boolean). Output: out = ! (in1 & in2), defined with zero delay. No initial states defined; all 4 input combinations are initial. Transitions are unconstrained; any state can transition to any other.

NAND Gate With Unit Delay

Example 
MODULE main
VAR
  in1 : boolean;
  in2 : boolean;
  out : boolean;

ASSIGN
  init(out) := TRUE;
  next(out) := !(in1 & in2);

Behavior and Transitions

3. Modular and Hierarchical Designs

MODULE nand2(in1, in2)
VAR
  out : boolean;

ASSIGN
  init(out) := TRUE;
  next(out) := !(in1 & in2);

MODULE main
VAR
  input1 : boolean;
  input2 : boolean;
  q : nand2(input1, input2);

Using Multiple NAND Modules

Modules becomes more useful while reusing components.

Instantiate two NAND modules q1 and q2 with inputs (x1, x2) and (y1, y2). Output computed as XOR of q1.out and q2.out.

Example 
MODULE main
VAR
  x1 : boolean; x2 : boolean;
  y1 : boolean; y2 : boolean;
  q1 : nand2(x1, x2);
  q2 : nand2(y1, y2);

DEFINE
  fout := q1.out xor q2.out;

MODULE nand2(in1, in2)
VAR
  out : boolean;

ASSIGN
  init(out) := TRUE;
  next(out) := !(in1 & in2);

Hierarchical NAND Circuit with Feedback

Two NAND gates connected in a feedback loop. Inputs x and y are boolean. Two variables q1 and q2 of nand2 type are instantiated with interdependent inputs.

Example 
MODULE main
VAR
  x : boolean;
  y : boolean;
  q1 : nand2(x, q2.out);
  q2 : nand2(q1.out, y);

DEFINE
  fout := q1.out xor q2.out;

MODULE nand2(in1, in2)
VAR
  out : boolean;

ASSIGN
  init(out) := TRUE;
  next(out) := !(in1 & in2);

NuSMV -int nand-demo5.smv
go
print_reachable_states -v
pick_state -i
simulate -i k 5

4. Example: 3-Bit Counter Using Modules

bit0 carryin is always TRUE. bit1 and bit2 carryin depend on previous bit's carryout. This constructs a synchronous 3-bit binary counter.

5. Summary

Part 3: Modeling Parallel Systems using NuSMV

We cover modeling synchronous and asynchronous parallel systems, mutual exclusion, and concurrent programs using NuSMV. We explore examples with traffic lights, mutual exclusion for shared resources, and concurrent programs manipulating a shared variable.

1. Introduction to Parallel Systems

2. Traffic Light Example: Synchronous vs Asynchronous Systems

alt text

System Description

Example 
MODULE light(other)
VAR
  state : {r, y, g};

ASSIGN
  init(state) := r;
  next(state) := case
    state = r & other = r : {r, y};
    state = y : g;
    state = g : {g, r};
    TRUE : state;
  esac;

MODULE main
VAR
  tl1 : light(tl2.state);
  tl2 : light(tl1.state);

Asynchronous Composition

Example 
MODULE main
VAR
  tl1 : process light(tl2.state);
  tl2 : process light(tl1.state);

NuSMV -int light_asyn_demo.smv
go
check_ltlspec -p "!( F (tl1.state=g & tl2.state = g))

Verification

-Property checked: Never both green simultaneously.

print_reachable_states -v
pick_state -i
simulate -i -k 3

3. Mutual Exclusion Example

Example 
MODULE thread(y)
VAR
  location : {nc, w, c, e};

ASSIGN
  init(location) := nc;
  next(location) := case
    location = nc : {nc, w};
    location = w & y > 0 : c;
    location = c : {c, e};
    location = e : nc;
    TRUE : location;
  esac;

  next(y) := case
    location = w & y > 0 : y - 1;
    location = e & y = 0 : y + 1;
    TRUE : y;
  esac;

MODULE main
VAR
  ymain : 0..1;
  p1 : process thread(ymain);
  p2 : process thread(ymain);

ASSIGN
  init(ymain) := 1;

Two parallel programs sharing a resource.

NuSMV -int mutex_demo1.smv
go
check_ltlspec -p "!F(p1.location=c & p2.location=c)"

Verification

pick_state -i
simulate -i -k 3

4. Concurrent Programs with Shared Variable

alt text

MODULE program1(x)
VAR
  location : {l1, l2};
ASSIGN
  init(location) := l1;
  next(location) := case
                    location = l1 & x < 200 : l2;
                    location = l2 : l1;
                    TRUE : location;
                  esac;

  next(x) := case
              location = l2 & x < 1000 : x + 1;
              TRUE : x;
            esac;

MODULE program2(x)
VAR
  location : {m1, m2};
ASSIGN
  init(location) := m1;
  next(location) := case
                  location = m1 & x > 0 : m2;
                  location = m2 : m1;
                  TRUE : location;
                esac;

  next(x) := case
              location = m2 & x > -1000 : x - 1;
              TRUE : x;
            esac;

MODULE program3(x)
VAR
  location : {n1, n2};
ASSIGN
  init(location) := n1;
  next(location) := case
                    location = n1 & x = 200 : n2;
                    location = n2 : n1;
                    TRUE : location;
                  esac;

  next(x) := case
              location = n2 : 0;
              TRUE : x;
            esac;

MODULE main
VAR
  x : -1000..1000;
  thread1 : process program1(x);
  thread2 : process program2(x);
  thread3 : process program3(x);
ASSIGN
  init(x) := 0;

NuSMV -int three_program_demo.smv
go 
check_ltlspec -p "G (x>=0)"

Verification

5. Summary