Unit-2: Model-checker NuSMV

(1)

Unit-2: Model-checker NuSMV

B. Srivathsan

Chennai Mathematical Institute

(2)

Module 2:

Simple models in NuSMV

(3)

l₁

l₂

MODULE main VAR

location: {l1,l2}; ASSIGN

init(location) := l1; next(location) := case

(location = l1) : l2; (location = l2) : l1;

esac;

(4)

l₁

l₂

MODULE main

VAR

location: {l1,l2}; ASSIGN

esac;

(5)

l₁

l₂

MODULE main VAR

location: {l1,l2};

ASSIGN

esac;

(6)

l₁

l₂

MODULE main VAR

location: {l1,l2};

ASSIGN

init(location) := l1;

next(location) := case

esac;

(7)

l₁

l₂

MODULE main VAR

location: {l1,l2};

ASSIGN

(location = l1) : l2;

esac;

(8)

l₁

l₂

x < 10 x := x+1

MODULE main VAR

location: {l1,l2};

x: 0 .. 100;

ASSIGN

init(x) := 0;

(location = l1): l2;

(location = l1) & (x<10): l2;

TRUE: location;

esac;

next(x) := case

(location = l2) & x < 100: x+1; TRUE: x;

esac;

(9)

l₁

l₂

x < 10 x := x+1

MODULE main VAR

location: {l1,l2};

x: 0 .. 100;

ASSIGN

init(x) := 0;

(location = l1) & (x<10): l2;

TRUE: location;

esac;

next(x) := case

esac;

(10)

l₁

l₂

x < 10 x := x+1

MODULE main VAR

location: {l1,l2};

x: 0 .. 100;

ASSIGN

init(x) := 0;

(location = l1) & (x<10): l2;

TRUE: location;

esac;

next(x) := case

esac;

(11)

l₁

l₂

x < 10 x := x+1

MODULE main VAR

location: {l1,l2};

x: 0 .. 100;

ASSIGN

init(x) := 0;

(location = l1) & (x<10): l2;

TRUE: location;

esac;

next(x) := case

esac;

(12)

l₁

l₂

x < 10 x := x+1

MODULE main VAR

location: {l1,l2};

x: 0 .. 100;

ASSIGN

init(x) := 0;

(location = l1) & (x<10): l2;

TRUE: location;

esac;

next(x) := case

esac;

(13)

l₁

l₂

x < 10 x := x+1

MODULE main VAR

location: {l1,l2};

x: 0 .. 100;

ASSIGN

init(x) := 0;

(location = l1) & (x<10): l2;

TRUE: location;

esac;

next(x) := case

esac;

(14)

l₁

l₂

x < 10 x := x+1

MODULE main VAR

location: {l1,l2};

x: 0 .. 100;

ASSIGN

init(x) := 0;

(location = l1) & (x<10): l2;

TRUE: location;

esac;

next(x) := case

(location = l2) & x < 100: x+1;

TRUE: x;

esac;

(15)

request=1

ready request=1

busy

request=0

ready request=0

busy

MODULE main VAR

request: boolean;

status: {ready, busy}

ASSIGN

init(status) := ready; next(status) := case

request : busy; TRUE : {ready,busy};

esac;

(16)

request=1

ready request=1

busy

request=0

ready request=0

busy

MODULE main VAR

request: boolean;

ASSIGN

init(status) := ready; next(status) := case

esac;

(17)

request=1

ready request=1

busy

request=0

ready request=0

busy

MODULE main VAR

request: boolean;

ASSIGN

init(status) := ready;

next(status) := case

esac;

(18)

request=1

ready request=1

busy

request=0

ready request=0

busy

MODULE main VAR

request: boolean;

ASSIGN

request : busy;

TRUE : {ready,busy};

esac;

(19)

request=1

ready request=1

busy

request=0

ready request=0

busy

MODULE main VAR

request: boolean;

ASSIGN

request : busy;

esac;

(20)

request=1

ready request=1

busy

request=0

ready request=0

busy

MODULE main VAR

request: boolean;

ASSIGN

request : busy;

esac;

(21)

Coming next: checking requirements in NuSMV

(22)

l₁

l₂

x < 10 x := x+1

Executions

l₁,x=0 l₂,x=0 l₁,x=1 l₂,x=1

l₁,x=9 l₂,x=9 l₁,x=10

...

(23)

request=1

ready request=1

busy

request=0

ready request=0

busy

Executions

request=0 ready

request=0 busy

request=0 ready

request=1 busy

request=1 ready

request=1 busy

request=0 busy

request=1 busy

request=0 ready

...

(24)

Transition system satisfies a requirement means

all its executions satisfy the requirement

(25)

Requirement type 1: G

G (x >= 0)

TS of above PG with initial value x=0 satisfies G (x >= 0)

l₁

l₂

x < 10 x := x+1

l₁,x=0 l₂,x=0 l₁,x=1 l₂,x=1

l₁,x=9 l₂,x=9 l₁,x=10

...

(26)

G (x >= 0)

l₁

l₂

x < 10 x := x+1

l₁,x=0 l₂,x=0 l₁,x=1 l₂,x=1

l₁,x=9 l₂,x=9 l₁,x=10

...

(27)

G (x >= 0)

l₁

l₂

x < 10 x := x+1

l₁,x=0 l₂,x=0 l₁,x=1 l₂,x=1

l₁,x=9

...

(28)

request=1

ready request=1

busy

request=0

ready request=0

busy

8/7

G (request=0)

× × Ø

TS does not satisfy G (request=0)

request=0 ready

request=0 busy

request=0 ready

request=1 busy

...

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

request=0 ready

...

(29)

request=1

ready request=1

busy

request=0

ready request=0

busy

G (request=0)

×

× Ø

TS does not satisfy G (request=0)

request=0 ready

request=0 busy

request=0 ready

request=1 busy

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

(30)

request=1

ready request=1

busy

request=0

ready request=0

busy

8/7

G (request=0)

× ×

Ø

TS does not satisfy G (request=0)

request=0 ready

request=0 busy

request=0 ready

request=1 busy

...

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

request=0 ready

...

(31)

request=1

ready request=1

busy

request=0

ready request=0

busy

G (request=0)

× × Ø

TS does not satisfy G (request=0)

request=0 ready

request=0 busy

request=0 ready

request=1 busy

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

(32)

request=1

ready request=1

busy

request=0

ready request=0

busy

8/7

G (request=0)

× × Ø

TS does not satisfy G (request=0)

request=0 ready

request=0 busy

request=0 ready

request=1 busy

...

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

request=0 ready

...

(33)

...

T T T T T T

Execution satisfies G (expr) if expr evaluates to T in all its states

Transition system satisfies G (expr) if

all its executions satisfy G (expr)

(34)

...

T T T T T T

Execution satisfies G (expr) if expr evaluates to T in all its states

Transition system satisfies G (expr) if

all its executions satisfy G (expr)

(35)

Checking the G requirement: NuSMV demo

(36)

Requirement type 2: F

F (x >= 5)

TS of above PG with initial value x=0 satisfies F (x >= 5)

l₁

l₂

x < 10 x := x+1

l₁,x=0 l₂,x=0 l₁,x=1 l₂,x=1

l₁,x=9 l₂,x=9 l₁,x=10

...

(37)

F (x >= 5)

TS of above PG with initial value x=0 satisfies F (x >= 5)

l₁

l₂

x < 10 x := x+1

l₁,x=0 l₂,x=0 l₁,x=1 l₂,x=1

l₁,x=9

...

(38)

F (x >= 5)

TS of above PG with initial value x=0 satisfies F (x >= 5)

l₁

l₂

x < 10 x := x+1

l₁,x=0 l₂,x=0 l₁,x=1 l₂,x=1

l₁,x=9 l₂,x=9 l₁,x=10

...

(39)

request=1

ready request=1

busy

request=0

ready request=0

busy

F (request=1)

Ø Ø ×

TS does not satisfy F (request=1)

request=0 ready

request=0 busy

request=0 ready

request=1 busy

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

(40)

request=1

ready request=1

busy

request=0

ready request=0

busy

8/7

F (request=1)

Ø

Ø ×

TS does not satisfy F (request=1)

request=0 ready

request=0 busy

request=0 ready

request=1 busy

...

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

request=0 ready

...

(41)

request=1

ready request=1

busy

request=0

ready request=0

busy

F (request=1)

Ø Ø

×

TS does not satisfy F (request=1)

request=0 ready

request=0 busy

request=0 ready

request=1 busy

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

(42)

request=1

ready request=1

busy

request=0

ready request=0

busy

8/7

F (request=1)

Ø Ø ×

TS does not satisfy F (request=1)

request=0 ready

request=0 busy

request=0 ready

request=1 busy

...

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

request=0 ready

...

(43)

request=1

ready request=1

busy

request=0

ready request=0

busy

F (request=1)

Ø Ø ×

TS does not satisfy

request=0 ready

request=0 busy

request=0 ready

request=1 busy

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

(44)

...

T

Execution satisfies F (expr) if expr evaluates to T in one of its states

Transition system satisfies F (expr) if

all its executions satisfy F (expr)

(45)

...

T

Execution satisfies F (expr) if expr evaluates to T in one of its states

Transition system satisfies F (expr) if

(46)

Checking the F requirement: NuSMV demo

(47)

Coming next: Combining G and F

(48)

request=1

ready request=1

busy

request=0

ready request=0

busy

8/7

G (request=1 => F status=busy)

Ø Ø Ø

TS satisfies

G (request => F (status=busy))

request=0 ready

request=0 busy

request=0 ready

request=1 busy

...

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

request=0 ready

...

(49)

request=1

ready request=1

busy

request=0

ready request=0

busy

Ø

Ø Ø

TS satisfies

request=0 ready

request=0 busy

request=0 ready

request=1 busy

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

(50)

request=1

ready request=1

busy

request=0

ready request=0

busy

8/7

Ø Ø

Ø

TS satisfies

request=0 ready

request=0 busy

request=0 ready

request=1 busy

...

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

request=0 ready

...

(51)

request=1

ready request=1

busy

request=0

ready request=0

busy

Ø Ø Ø

TS satisfies

request=0 ready

request=0 busy

request=0 ready

request=1 busy

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

(52)

request=1

ready request=1

busy

request=0

ready request=0

busy

8/7

Ø Ø Ø

TS satisfies

request=0 ready

request=0 busy

request=0 ready

request=1 busy

...

request=1 ready

request=1 busy

request=0 ready

request=1 busy

request=0 ready

...

request=0 ready

...

(53)

Summary

Using NuSMV

Format for writing models

G and F requirements