MTech Computer Science and Engg Formal Model in computer science programs
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:
For instance,
for a system running windows vista on a 32 machine you can paste this in your
web browser:
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))
Subscribe to:
Posts (Atom)