MTECH TEXT BOOKS, QUESTION PAPERS, LAB PROGRAMS,IEEE PAPERS

Hi,

Software Requirements:

1 .NuSMV

2. Alloy

Installing and using NuSMV (under Windows)

1. Go to the address below and chose an installation file according to your system version:

http://nusmv.fbk.eu/bin/bin_download2-v2.cgi

For instance, for a system running windows vista on a 32 machine you can paste this in your web browser:

http://nusmv.fbk.eu/distrib/NuSMV-2.5.2-i586-pc-mingw32msvc.exe

2. Open the download directory and run the executable (by double-clicking on the file, for instance). Do the following during the installation wizard:

a. click 'Proceed',

b. click 'Next'

c. choose a location, for instance: Browse ! Desktop, (the default installation directory is 'C/Program Files/NuSMV') and click 'Install'

3. Open a command prompt (for instance by: Start ! All Programs !Accessories ! Command Prompt)

4. Go to your installation place (by writing at command prompt:)

cd \Desktop\nusmv\2.5.2\bin

5. Open your favorite text editor (by writing, for instance): notepad tictactoe.smv

6. Write and save your program (below you have a basic program template):

MODULE main

VAR

variable : boolean;

ASSIGN

init(variable) := TRUE;

next(variable) := !variable;

LTLSPEC

G (variable & X !variable)

CTLSPEC

EF (!variable & AX variable)

7. Run your program to check the assertions from the specifications section,

by writing the following at the command prompt:

NuSMV.exe tictactoe.smv

8. This will produce the following output:

-- specification EF (!variable & AX variable) is true

-- specification G (variable & X !variable) is false

-- as demonstrated by the following execution sequence

Trace Description: LTL Counterexample

Trace Type: Counterexample

-- Loop starts here

-> State: 1.1 <-

variable = TRUE

-> State: 1.2 <-

variable = FALSE

-> State: 1.3 <-

variable = TRUE

9. Include the program code in your (.tex) assignment file and you are done.

Installing and using ALLOY (under Windows)

1. Download and Install Java Developer Kit 6 (JDK 6).

2. Now download the alloy4.jar file (available at alloy.mit.edu) then double-click on the jar file, or type:

java -jar alloy4.jar in the console.

------------------------------------------------------------------------------------------------------------1. Design, develop and run a program in ALLOY (or in any equivalent system) to model a Software Package Dependency System. Make suitable assumptions regarding the system. The model should allow checking to see if prerequisites in the form of libraries or other packages are present for all components in the system.

module PDS

open std/ord -- opens specification template for linear order

sig Component

{

name: Name,

main: option Service,

export: set Service,

import: set Service,

version: Number

}

{

no import & export

}

sig PDS

{

components: set Component,

schedule: components -> Service ->? components,

requires: components -> components

}

{

components.import in components.export

}

fact SoundPDSs

{

all P : PDS | with P

{

all c : components, s : Service | let c’ = c.schedule[s]

{

(some c’ iff s in c.import) && (some c’ => s in c’.export)

}

all c : components | c.requires = c.schedule[Service]

}

sig Name, Number, Service {}

fun AddComponent(P, P’: PDS, c: Component)

{

not c in P.components

P’.components = P.components + c

}

run AddComponent for 3 but 2 PDS

fun RemoveComponent(P, P’: PDS, c : Component)

{

c in P.components

P’.components = P.components - c

}

run RemoveComponent for 3 but 2 PDS

fun HighestVersionPolicy(P: PDS)

{

with P

{

all s : Service, c : components, c’ : c.schedule[s],

c’’ : components - c’

{

s in c’’.export && c’’.name = c’.name =>

c’’.version in c’.version.^(Ord[Number].prev)

}

run HighestVersionPolicy for 3 but 1 PDS

fun AGuidedSimulation(P,P’,P’’ : PDS, c1, c2 : Component)

{

AddComponent(P,P’,c1) RemoveComponent(P,P’’,c2)

HighestVersionPolicy(P)

HighestVersionPolicy(P’)

HighestVersionPolicy(P’’)

}

run AGuidedSimulation for 3

assert AddingIsFunctionalForPDSs

{

all P, P’, P’’: PDS, c: Component

{

AddComponent(P,P’,c) &&

AddComponent(P,P’’,c) => P’ = P’’

}

check AddingIsFunctionalForPDSs for 3

------------------------------------------------------------------------------------------------------------

2. Design, develop and run a program in NuSMV (or in any equivalent system) to model and solve the Mutual Exclusion problem.

MODULE main

VAR

pr1: process prc(pr2.st, turn, 0);

pr2: process prc(pr1.st, turn, 1);

turn: boolean;

ASSIGN

init(turn) := 0;

-- safety

LTLSPEC G!((pr1.st = c) & (pr2.st = c))

-- liveness

LTLSPEC G((pr1.st = t) -> F (pr1.st = c))

LTLSPEC G((pr2.st = t) -> F (pr2.st = c))

-- ‘negation’ of strict sequencing (desired to be false)

LTLSPEC G(pr1.st=c -> ( G pr1.st=c | (pr1.st=c U

(!pr1.st=c & G !pr1.st=c | ((!pr1.st=c) U pr2.st=c)))))

MODULE prc(other-st, turn, myturn)

VAR

st: {n, t, c};

ASSIGN

init(st) := n;

next(st) :=

case

(st = n) : {t,n};

(st = t) & (other-st = n) : c;

(st = t) & (other-st = t) & (turn = myturn) : c;

(st = c) : {c,n};

1 : st;

esac;

next(turn) :=

case

turn = myturn & st = c : !turn;

1 : turn;

esac;

FAIRNESS running

FAIRNESS !(st = c)

-----------------------------------------------------------------------------------------------------------

3. Design, develop and run a program in NuSMV (or in any equivalent system) to model and simulate the Alterate Bit Protocol.

The ABP sender in SMV:

MODULE sender (ack)

VAR

st : {sending,sent};

message1 : boolean;

message2 : boolean;

ASSIGN

init(st) := sending;

next(st) := case

ack = message2 & !(st=sent) : sent;

1 : sending;

esac;

next(message1) :=

case

st = sent : {0,1};

1 : message1;

esac;

next(message2) :=

case

st = sent : !message2;

1 : message2;

esac;

FAIRNESS running

LTLSPEC G F st=sent

The ABP receiver in SMV:

MODULE receiver (message1,message2)

VAR

st : {receiving,received};

ack : boolean;

expected : boolean;

ASSIGN

init(st) := receiving;

next(st) := case

message2=expected & !(st=received) : received;

1 : receiving;

esac;

next(ack) :=

case

st = received : message2;

1 : ack;

esac;

next(expected) :=

case

st = received : !expected;

1 : expected;

esac;

FAIRNESS running

LTLSPEC G F st=received

------------------------------------------------------------------------------------------------------------

4. Design, develop and run a program in NuSMV (or in any equivalent system) to model and solve the planning problem of Ferry Man.

MODULE main

VAR

Ferryman : boolean;

Goat : boolean;

Cabbage : boolean;

Wolf : boolean;

Carry : {g,c,w,0};

ASSIGN

init(ferryman) := 0; init(goat) := 0;

init(cabbage) := 0; init(wolf) := 0;

init(carry) := 0;

next(ferryman) := 0,1;

next(carry) := case

ferryman=goat : g;

1 :0;

esac union

case

ferryman=cabbage : c;

1 :0;

esac union

case

ferryman=wolf : w;

1 :0;

esac union 0;

next(goat) := case

ferryman=goat & next(carry)=g : next(ferryman);

1 :goat;

esac;

next(cabbage) := case

ferryman=cabbage & next(carry)=c : next(ferryman);

1 :cabbage;

esac;

next(wolf) := case

ferryman=wolf & next(carry)=w : next(ferryman);

1 :wolf;

esac;

Output:

LTLSPEC !(( (goat=cabbage | goat=wolf) -> goat=ferryman)

U (cabbage & goat & wolf & ferryman))

acws-0116% nusmv ferryman.smv

*** This is NuSMV 2.1.2 (compiled 2002-11-22 12:00:00)

*** For more information of NuSMV see <http://nusmv.irst.itc.it>

*** or email to <nusmv-users@irst.itc.it>.

*** Please report bugs to <nusmv-users@irst.itc.it>.

-- specification !(((goat = cabbage | goat = wolf) -> goat = ferryman)

U (((cabbage & goat) & wolf) & ferryman)) is false

-- as demonstrated by the following execution sequence

-- loop starts here --

-> State 1.1 <-

ferryman = 0 -> State 1.8 <-

goat = 0 ferryman = 1

cabbage = 0 goat = 1

wolf = 0 carry = g

carry = 0 -> State 1.9 <-

-> State 1.2 <- -> State 1.10 <-

ferryman = 1 ferryman = 0

goat = 1 cabbage = 0

carry = g carry = c

-> State 1.3 <- -> State 1.11 <-

ferryman = 0 ferryman = 1

carry = 0 carry = 0

-> State 1.4 <- -> State 1.12 <-

ferryman = 1 ferryman = 0

cabbage = 1 wolf = 0

carry = c carry = w

-> State 1.5 <- -> State 1.13 <-

ferryman = 0 ferryman = 1

goat = 0 carry = 0

carry = g ->State 1.14 <-

-> State 1.6 <- ferryman = 0

ferryman = 1 goat = 0

wolf = 1 carry = g

carry = w -> State 1.15 <-

-> State 1.7 <- carry = 0

ferryman = 0

carry = 0

------------------------------------------------------------------------------------------------------------

5. Design, develop and run a program in NuSMV (or in any equivalent system) to model and solve the Dining Philosophers Problem.

MODULE main

VAR

forks : array 0..4 of {nobody,0,1,2,3,4};

p0 : process philosopher(0,forks[0],forks[1]);

p1 : process philosopher(1,forks[1],forks[2]);

p2 : process philosopher(2,forks[2],forks[3]);

p3 : process philosopher(3,forks[3],forks[4]);

p4 : process philosopher(4,forks[4],forks[0]);

ASSIGN

init(forks[0]) := nobody;

init(forks[1]) := nobody;

init(forks[2]) := nobody;

init(forks[3]) := nobody;

init(forks[4]) := nobody;

MODULE philosopher(i,left,right)

VAR

state : {thinking, hungry, eating, done};

-- done state is used to drop the forks properly

DEFINE

gotleft := (left=i);

gotright := (right=i);

leftfree := (left=nobody);

rightfree := (right=nobody);

ASSIGN

init(state) := thinking;

next(left) :=

case

(state = done) : nobody; -- drop fork

!leftfree : left; -- can't grab if not free

leftfree & (state=hungry) : i; -- grab fork

1 : left;

esac;

next(right) :=

case

(state = done) : nobody; -- drop fork

!gotleft : right; -- grab left one first

!rightfree : right; -- can't grab if not free

rightfree & (state=hungry) : i; -- grab fork

1 : right;

esac;

next(state) :=

case

(state=thinking) : {thinking, hungry};

(state=hungry) & gotleft & gotright : eating;

(state=hungry) : hungry; -- don't have forks

(state=eating) : {eating, done};

(state=done) : thinking;

1 : state;

esac;

FAIRNESS

running

SPEC

-- must have both forks to eat

AG ((state = eating) -> (gotleft)&(gotright))

SPEC

-- if hungry, must eventually get to eat

AG ((state = hungry) -> AF (state = eating))

-----------------------------------------------------------------------------------------------------------

MTECH TEXT BOOKS, QUESTION PAPERS, LAB PROGRAMS,IEEE PAPERS

M.Tech CSE TEXT BOOKS

M.Tech First sem CSE Text Books

M.Tech Second sem CSE Text Books

M.Tech Third sem CSE Text Books

POST GRADUATION DETAILS

PG DETAILS CLICK ME!!

VTU Website

PG CET 2010 PAPER

VLSI TEXT BOOX

APTITUDE MATERIALS

APTITUDE MATERIALS

IEEE PAPERS

CLOUD COMPUTING

DATA MINING

IMAGE PROCESSING

NETWORKS

ACA and OTHER MATERIALS

MULTIMEDIA

MULTIMEDIA

MULTIMEDIA QUESTION PAPER

INS and SAN

Formal Model Computer Science

Advance Algorithm Question paper(MTech 2nd sem)

MTech Computer Science and Engg Formal Model in computer science programs