Overture Tool
Formal Modelling in VDM
CashDispenserConcPP
Author: Sten Agerholm, Peter Gorm Larsen and Kim Sunesen
This model is concurrent and it is described in VDM++. This enables abstraction from design considerations and can model errors in the communication channel and it ensures maximum focus on high-level, precise and systematic analysis. This was developed by Sten Agerholm, Peter Gorm Larsen and Kim Sunesen in 1999 in connection with FM’99.
| Properties | Values |
|---|---|
| Language Version: | vdm10 |
| Entry point : | new Main().Run() |
LocalResource.vdmpp
class LocalResource
instance variables
c : Channel := new Channel();
operations
public LocalResource : Channel ==> LocalResource
LocalResource(nc) ==
c := nc;
public GetBalance : Account`AccountId ==> [nat]| <Fail>
GetBalance(accountId) ==
let req = mk_Channel`Request(<GetBalance>,
{mk_Channel`AccountId(accountId)}) in
(c.SendRequest(req);
Wait(<GetBalance>));
Wait : Channel`Command ==> Channel`RespData | <Fail>
Wait(comm) ==
(c.Wait();
let resp = c.ReceiveResponse() in
if resp = nil
then return <Fail>
elseif resp.command <> comm
then return <Fail>
else return resp.data);
public Withdrawal : Account`AccountId * Card`CardId * nat ==> bool | <Fail>
Withdrawal(accountId,cardId,amount) ==
let req = mk_Channel`Request(<Withdrawal>,
{mk_Channel`AccountId(accountId),
mk_Channel`CardId(cardId),
mk_Channel`Amount(amount)}) in
(c.SendRequest(req);
Wait(<Withdrawal>));
public PostStatement : Account`AccountId * Card`CardId ==> bool | <Fail>
PostStatement(accountId,cardId) ==
let req = mk_Channel`Request(<PostStmt>,
{mk_Channel`AccountId(accountId),
mk_Channel`CardId(cardId)}) in
(c.SendRequest(req);
Wait(<PostStmt>));
public IsLegalCard : Account`AccountId * Card`CardId ==> bool | <Fail>
IsLegalCard(accountId,cardId) ==
let req = mk_Channel`Request(<IsLegalCard>,
{mk_Channel`AccountId(accountId),
mk_Channel`CardId(cardId)}) in
(c.SendRequest(req);
Wait(<IsLegalCard>));
public NumberOfTriesExceeded : Card`CardId ==> bool | <Fail>
NumberOfTriesExceeded(cardId) ==
let req = mk_Channel`Request(<TriesExceeded>,
{mk_Channel`CardId(cardId)}) in
(c.SendRequest(req);
Wait(<TriesExceeded>));
public ResetNumberOfTries : Card`CardId ==> [<Fail>]
ResetNumberOfTries(cardId) ==
let req = mk_Channel`Request(<ResetTries>,
{mk_Channel`CardId(cardId)}) in
(c.SendRequest(req);
Wait(<ResetTries>));
public IncrNumberOfTries : Card`CardId ==> [<Fail>]
IncrNumberOfTries(cardId) ==
let req = mk_Channel`Request(<IncTries>,
{mk_Channel`CardId(cardId)}) in
(c.SendRequest(req);
Wait(<IncTries>));
end LocalResource
Letter.vdmpp
class Letter
instance variables
name : Cardholder`Name;
address : Cardholder`Address;
date : Clock`Date;
transactions : seq of Account`Transaction;
balance : nat
operations
public Letter: Cardholder`Name * Cardholder`Address * Clock`Date *
seq of Account`Transaction * nat ==> Letter
Letter(nm,addr,d,ts,b) ==
(name := nm;
address := addr;
date := d;
transactions := ts;
balance:= b)
end Letter
Letterbox.vdmpp
class Letterbox
instance variables
statements : seq of Letter := [];
operations
public PostStatement : Letter ==> ()
PostStatement(letter) ==
statements := statements ^ [letter];
pure GetLastStatement : () ==> Letter
GetLastStatement() ==
return statements(len statements)
pre statements <> [];
end Letterbox
concur.vdmpp
class Main
instance variables
ltills : map TillId to LocalTill := {|->};
tills : map TillId to Till := {|->};
cards : seq of Card := [];
resource : CentralResource;
clock : Clock := new Clock();
letterbox : Letterbox := new Letterbox();
mb : MessageBuffer := new MessageBuffer();
types
public TillId = nat;
values
nat2char : map nat to char =
{ 0 |-> '0', 1 |-> '1', 2 |-> '2', 3 |-> '3', 4 |-> '4',
5 |-> '5', 6 |-> '6', 7 |-> '7', 8 |-> '8', 9 |-> '9' };
functions
tStr : nat -> seq of char
tStr(n) == "Till " ^ nat2string(n) ^":\t";
nat2chars : nat -> seq of char
nat2chars(n) ==
if n = 0
then []
elseif n < 10
then [nat2char(n)]
else (nat2chars(n div 10)) ^ [ nat2char(n mod 10)];
nat2string : nat -> seq of char
nat2string(n) ==
if n = 0
then "0"
else nat2chars(n)
operations
pure public GetTill: TillId ==> Till
GetTill(tid) ==
return tills(tid);
public Main: () ==> Main
Main() ==
(clock.SetDate("150999");
let c1 = new Card(123456,1,1),
c2 = new Card(123457,2,2),
c3 = new Card(123458,3,3),
c4 = new Card(123459,4,4),
c5 = new Card(123460,5,5),
c6 = new Card(123461,6,5),
c7 = new Card(123462,7,5)
in
let peter = new Cardholder("Peter Gorm Larsen",
"Granvej 24"),
paul = new Cardholder("Paul Mukherjee",
"Rugaardsvej 47"),
sten = new Cardholder("Sten Agerholm",
"Teisensvej ??"),
kim = new Cardholder("Kim Sunesen",
"??"),
CSK = new Cardholder("CSK","Forskerparken 10A")
in
let pglacc1 = new Account({1 |-> peter},5000),
saacc1 = new Account({2 |-> sten},0),
ksacc1 = new Account({3 |-> kim},9000),
pmacc1 = new Account({4 |-> paul},6000),
ifacc1 = new Account({5 |-> peter,
6 |-> sten,
7 |-> CSK},3000),
pglid1 = 1,
said1 = 2,
ksid1 = 3,
pmid1 = 4,
ifid1 = 5
in
(resource := new CentralResource(clock,new Letterbox());
resource.AddAccount(pglid1,pglacc1);
resource.AddAccount(said1,saacc1);
resource.AddAccount(ksid1,ksacc1);
resource.AddAccount(pmid1,pmacc1);
resource.AddAccount(ifid1,ifacc1);
tills := {1 |-> SetupTill(1,new Till()),
2 |-> SetupTill(2,new Till()),
3 |-> SetupTill(3,new Till()),
4 |-> SetupTill(4,new Till())};
cards := [c1,c2,c3,c4,c5,c6,c7];
));
SetupTill : nat * Till ==> Till
SetupTill(i,t) ==
let c = new Channel(),
lt = new LocalTill(c, resource),
lr = new LocalResource(c) in
(start(lt);
ltills := ltills ++ { i |-> lt};
t.Set(lr));
public RepairTill : nat ==> ()
RepairTill(tillNum) ==
tills(tillNum) := SetupTill(tillNum, tills(tillNum));
public EnterCardAtTill : nat * nat * nat ==> ()
EnterCardAtTill(tillNum, cardNum, pin) ==
(tills(tillNum).InsertCard(cards(cardNum));
let validRes1 = tills(tillNum).Validate(pin) in
let msg = cases validRes1:
<Fail> -> tStr(tillNum) ^"Validate card failed",
<Retained> -> tStr(tillNum) ^"Card Retained",
<PinNotOk> -> "Validate Unsuccessful",
<PinOk> -> tStr(tillNum) ^"Validate Successful",
others -> tStr(tillNum) ^"Unknown Message"
end in
mb.put(msg);
-- Make till 1 fail as soon as the card is entered
if tillNum = 1
then Fail(tillNum))
pre tillNum in set dom tills;
public WithdrawalAtTill : nat * nat ==> ()
WithdrawalAtTill(tillNum, amount) ==
let wd1 = tills(tillNum).MakeWithdrawal(amount) in
let msghdr =tStr(tillNum) ^"Withdrawal ("^nat2string(amount) ^")" in
if <Fail> = wd1
then mb.put(msghdr ^ " Failed")
elseif not wd1
then mb.put(msghdr ^ " Unsuccessful")
else mb.put(msghdr ^ " Successful");
public GetBalanceAtTill : nat ==> ()
GetBalanceAtTill (tillNum) ==
let bal1 = tills(tillNum).GetBalance() in
if nil = bal1
then mb.put(tStr(tillNum) ^
"Balance not known for this account")
elseif <Fail> = bal1
then mb.put(tStr(tillNum) ^"Balance Failed")
else mb.put(tStr(tillNum) ^
"Balance is " ^ nat2string(bal1) );
public Fail : nat ==> ()
Fail(tillNum) ==
(ltills(tillNum).Fail();
mb.put(tStr(tillNum) ^ "LocalTill Fail"));
public ReturnCard : nat ==> ()
ReturnCard(tillNum) ==
(tills(tillNum).ReturnCard();
mb.put(tStr(tillNum) ^"Card Returned"));
Wait: () ==> ()
Wait () == skip;
public Run : () ==> seq of char
Run() ==
(dcl user1:User := new User(1,1,123456,self),
user2:User := new User(2,5,123460,self),
user3:User := new User(3,6,123461,self),
user4:User := new User(4,7,123462,self);
start(user1);
start(user2);
start(user3);
start(user4);
Wait();
return mb.get());
sync
mutex(SetupTill);
mutex(ReturnCard);
per Wait => #fin(ReturnCard) >= 3
end Main
class MessageBuffer
instance variables
data : seq of char := [];
operations
public put : seq of char ==> ()
put(msg) ==
data := data ^ "\n" ^ msg ;
public get : () ==> seq of char
get() == return data;
sync
mutex(all);
end MessageBuffer
class User
instance variables
tillNum : nat;
cardNum : nat;
pin : nat;
m : Main
operations
public User : nat * nat * nat * Main ==> User
User (nt, nc, np, nm) ==
(tillNum := nt;
cardNum := nc;
pin := np;
m := nm);
Test1 : () ==> ()
Test1() ==
(m.EnterCardAtTill(tillNum,cardNum,pin);
m.GetBalanceAtTill(tillNum);
m.WithdrawalAtTill(tillNum,100);
m.GetBalanceAtTill(tillNum);
m.ReturnCard(tillNum))
thread
Test1()
end User
Till.vdmpp
class Till
instance variables
curCard : [Card] := nil;
cardOk : bool := false;
retainedCards : set of Card := {};
resource : LocalResource;
inv curCard = nil => not cardOk;
operations
public Till: LocalResource ==> Till
Till(res) ==
resource := res;
public Set: LocalResource ==> Till
Set(res) ==
(resource := res;
return self);
public InsertCard : Card ==> ()
InsertCard(c) ==
curCard := c
pre not CardInside();
public Validate : Card`PinCode ==> <PinOk> | <PinNotOk> | <Retained>
| <Fail>
Validate(pin) ==
let cardId = curCard.GetCardId(),
codeOk = curCard.GetCode() = Encode(pin),
cardLegal = IsLegalCard()
in if cardLegal = <Fail>
then return <Fail>
else
(cardOk := codeOk and cardLegal;
if not cardLegal
then (retainedCards := retainedCards union {curCard};
curCard := nil;
return <Retained>)
elseif codeOk
then if resource.ResetNumberOfTries(cardId) = <Fail>
then return <Fail>
else return <PinOk>
else
(let incTries = resource.IncrNumberOfTries(cardId),
numTriesExceeded =
resource.NumberOfTriesExceeded(cardId) in
if <Fail> in set {incTries, numTriesExceeded}
then return <Fail>
elseif numTriesExceeded then
(retainedCards := retainedCards union {curCard};
cardOk := false;
curCard := nil;
return <Retained>)
else return <PinNotOk>
)
)
pre CardInside() and not cardOk;
public ReturnCard : () ==> ()
ReturnCard() ==
(cardOk := false;
curCard:= nil)
pre CardInside();
public GetBalance : () ==> [nat]|<Fail>
GetBalance() ==
resource.GetBalance(curCard.GetAccountId())
pre CardValidated();
public MakeWithdrawal : nat ==> bool | <Fail>
MakeWithdrawal(amount) ==
resource.Withdrawal
(curCard.GetAccountId(),curCard.GetCardId(),amount)
pre CardValidated();
public RequestStatement : () ==> bool | <Fail>
RequestStatement() ==
resource.PostStatement(curCard.GetAccountId(),curCard.GetCardId())
pre CardValidated();
public IsLegalCard : () ==> bool | <Fail>
IsLegalCard() ==
return
resource.IsLegalCard(curCard.GetAccountId(),curCard.GetCardId())
pre CardInside();
pure public CardValidated: () ==> bool
CardValidated() ==
return curCard <> nil and cardOk;
pure public CardInside: () ==> bool
CardInside() ==
return curCard <> nil;
functions
Encode: Card`PinCode +> Card`Code
Encode(pin) ==
pin; -- NB The actual encoding procedure has not yet been chosen
end Till
Card.vdmpp
class Card
types
public CardId = nat;
public Code = nat;
public PinCode = nat;
instance variables
code : Code;
cardId : CardId;
accountId : Account`AccountId;
operations
public Card : Code * CardId * Account`AccountId ==> Card
Card(c,cid,a) ==
(code := c;
cardId := cid;
accountId := a);
pure public GetCode : () ==> Code
GetCode() ==
return code;
pure public GetAccountId : () ==> Account`AccountId
GetAccountId() ==
return accountId;
pure public GetCardId : () ==> CardId
GetCardId() ==
return cardId;
end Card
Timer.vdmpp
class Timer
instance variables
curTime : nat := 0;
active : bool := false;
operations
public Start : () ==> ()
Start() ==
(active := true;
curTime := 0);
public Stop : () ==> ()
Stop() ==
active := false;
pure public GetTime : () ==> nat
GetTime() ==
return curTime;
IncTime: () ==> ()
IncTime() ==
if active
then curTime := curTime + 100;
-- FIXME: Example used RT constructs must be rewritten using threads
--thread
-- periodic(1000)(IncTime)
end Timer
Account.vdmpp
class Account
instance variables
cards : map Card`CardId to Cardholder;
balance : nat;
transactions : seq of Transaction := [];
inv TransactionsInvariant(transactions);
values
dailyLimit : nat = 2000;
types
public AccountId = nat;
public Transaction :: date : Clock`Date
cardId : Card`CardId
amount : nat;
operations
public Account : map Card`CardId to Cardholder * nat ==> Account
Account(cs,b) ==
(cards := cs;
balance := b);
pure public GetBalance : () ==> nat
GetBalance() ==
return balance;
public Withdrawal : Card`CardId * nat * Clock`Date ==> bool
Withdrawal(cardId,amount,date) ==
let transaction = mk_Transaction(date,cardId,amount)
in
if balance - amount >= 0 and
DateTotal(date,transactions^[transaction]) <= dailyLimit
then
(balance := balance - amount;
transactions := transactions ^ [transaction];
return true)
else
return false
pre cardId in set dom cards;
pure public MakeStatement : Card`CardId * Clock`Date ==> Letter
MakeStatement(cardId,date) ==
let nm = cards(cardId).GetName(),
addr = cards(cardId).GetAddress()
in
return new Letter(nm,addr,date,transactions,balance)
pre cardId in set dom cards;
pure public GetCardIds: () ==> set of Card`CardId
GetCardIds() ==
return dom cards;
AddCard : Card`CardId * Cardholder ==> ()
AddCard(cId,ch) ==
cards := cards munion {cId |-> ch}
pre cId not in set dom cards;
functions
TransactionsInvariant: seq of Transaction +> bool
TransactionsInvariant(ts) ==
forall date in set {ts(i).date | i in set inds ts} &
DateTotal(date,ts) <= dailyLimit;
DateTotal : Clock`Date * seq of Transaction +> nat
DateTotal(date,ts) ==
Sum([ts(i).amount | i in set inds ts & ts(i).date = date]);
Sum: seq of real +> real
Sum(rs) ==
if rs = [] then 0
else
hd rs + Sum(tl rs)
measure Len;
Len: seq of real -> nat
Len(list) == len list
end Account
Channel.vdmpp
class Channel
instance variables
req : [Request] := nil;
resp :[Response] := nil;
timer : Timer := new Timer();
curTime : nat := 0;
values
timeout = 1500;
types
public Request :: command : Command
data : set of ReqData;
public Command = <TriesExceeded> | <ResetTries> | <IncTries> |
<GetBalance> | <Withdrawal> | <PostStmt> |
<IsLegalCard>;
public ReqData = CardId | AccountId | Amount;
public CardId :: val : Card`CardId;
public AccountId :: val : Account`AccountId;
public Amount :: val : nat;
public Response :: command : Command
data : RespData;
public RespData = [nat] | bool;
operations
public SendRequest : Request ==> ()
SendRequest(r) ==
(req := r;
timer.Start())
pre req = nil;
public ReceiveRequest : () ==> Request
ReceiveRequest() ==
let r = req in
(req := nil;
return r);
public SendResponse : Response ==> ()
SendResponse(r) ==
(resp := r;
timer.Stop())
pre resp = nil;
public ReceiveResponse : () ==> [Response]
ReceiveResponse() ==
let r = resp in
(resp := nil;
return r);
public Wait: () ==> ()
Wait() ==
skip;
CheckTime: () ==> ()
CheckTime() ==
curTime := timer.GetTime()
functions
AllReceived : nat * nat * nat * nat -> bool
AllReceived(act_send, fin_send, act_rec, fin_rec) ==
act_send = fin_send and
act_rec = fin_rec and
(act_send + fin_send) = (act_send + fin_send);
sync
per SendResponse =>
AllReceived(#act(SendRequest), #fin(SendRequest),
#act(ReceiveRequest), #fin(ReceiveRequest)) and
AllReceived(#act(SendResponse), #fin(SendResponse),
#act(ReceiveResponse), #fin(ReceiveResponse)) and
#act(SendRequest) - #fin(SendResponse) = 1;
per ReceiveRequest => req <> nil;
per Wait => curTime > timeout or resp <> nil;
-- FIXME: Example used RT constructs must be rewritten using threads
--thread
-- periodic(1000)(CheckTime)
end Channel
LocalTill.vdmpp
class LocalTill
instance variables
c: Channel;
resource : CentralResource;
enabled : bool := true;
thread
while enabled do
let req = c.ReceiveRequest() in
if enabled
then ProcessRequest(req);
operations
ProcessRequest : Channel`Request ==> ()
ProcessRequest(req) ==
(dcl respdata : Channel`RespData;
cases req:
mk_Channel`Request(
<Withdrawal>, {mk_Channel`AccountId(accId),
mk_Channel`CardId(cardId),
mk_Channel`Amount(amt)})
-> respdata := resource.Withdrawal(accId, cardId, amt),
mk_Channel`Request(
<PostStmt>, {mk_Channel`AccountId(accId),
mk_Channel`CardId(cardId)})
-> respdata := resource.PostStatement(accId, cardId),
mk_Channel`Request(
<IsLegalCard>, {mk_Channel`AccountId(accId),
mk_Channel`CardId(cardId)})
-> respdata := resource.IsLegalCard(accId, cardId),
mk_Channel`Request(
<GetBalance>, {mk_Channel`AccountId(accId)})
-> respdata := resource.GetBalance(accId),
mk_Channel`Request(
<TriesExceeded>, {mk_Channel`CardId(cardId)})
-> respdata := resource.NumberOfTriesExceeded(cardId),
mk_Channel`Request(
<ResetTries>, {mk_Channel`CardId(cardId)})
-> (resource.ResetNumberOfTries(cardId);
respdata := nil),
mk_Channel`Request(
<IncTries>, {mk_Channel`CardId(cardId)})
-> (resource.IncrNumberOfTries(cardId);
respdata := nil)
end;
c.SendResponse(mk_Channel`Response(req.command, respdata)));
public LocalTill : Channel * CentralResource ==> LocalTill
LocalTill(nc, nr) ==
(c := nc;
resource := nr);
public Fail : () ==> ()
Fail() ==
enabled := false;
public Repair : Channel ==> ()
Repair(nc) ==
(c := nc;
enabled := true);
end LocalTill
CentralResource.vdmpp
class CentralResource
instance variables
accounts : map Account`AccountId to Account := {|->};
numberOfTries : map Card`CardId to nat := {|->};
illegalCards : set of Card`CardId := {};
letterbox : Letterbox;
clock : Clock;
inv forall acc1,acc2 in set rng accounts &
acc1 <> acc2 =>
acc1.GetCardIds() inter acc2.GetCardIds() = {};
values
maxNumberOfTries : nat = 3;
operations
public CentralResource : Clock * Letterbox ==> CentralResource
CentralResource(c,l) ==
(clock := c;
letterbox := l);
pure public GetBalance : Account`AccountId ==> [nat]
GetBalance(accountId) ==
if accountId in set dom accounts then
accounts(accountId).GetBalance()
else
return nil;
public Withdrawal : Account`AccountId * Card`CardId * nat ==> bool
Withdrawal(accountId,cardId,amount) ==
if IsLegalCard(accountId,cardId) then
accounts(accountId).Withdrawal(cardId,amount,clock.GetDate())
else
return false;
public PostStatement : Account`AccountId * Card`CardId ==> bool
PostStatement(accountId,cardId) ==
if IsLegalCard(accountId,cardId) then
(letterbox.PostStatement
(accounts(accountId).MakeStatement(cardId,clock.GetDate()));
return true)
else
return false;
pure public IsLegalCard : Account`AccountId * Card`CardId ==> bool
IsLegalCard(accountId,cardId) ==
return
cardId not in set illegalCards and
accountId in set dom accounts and
cardId in set accounts(accountId).GetCardIds();
pure public NumberOfTriesExceeded : Card`CardId ==> bool
NumberOfTriesExceeded(cardId) ==
return numberOfTries(cardId) >= maxNumberOfTries;
public ResetNumberOfTries : Card`CardId ==> ()
ResetNumberOfTries(cardId) ==
numberOfTries(cardId) := 0;
public IncrNumberOfTries : Card`CardId ==> ()
IncrNumberOfTries(cardId) ==
numberOfTries(cardId) := numberOfTries(cardId) + 1;
public AddAccount : Account`AccountId * Account ==> ()
AddAccount(accId,acc) ==
(numberOfTries := numberOfTries ++
{cId |-> 0 | cId in set acc.GetCardIds()};
accounts := accounts ++ {accId |-> acc})
pre accId not in set dom accounts;
public AddIllegalCard : Card`CardId ==> ()
AddIllegalCard(cId) ==
illegalCards := illegalCards union {cId};
end CentralResource
CardHolder.vdmpp
class Cardholder
types
public Address = seq of char;
public Name = seq of char;
instance variables
name : Name;
address : Address;
operations
public Cardholder : Name * Address ==> Cardholder
Cardholder(nm,addr) ==
(name := nm;
address := addr);
pure public GetName : () ==> Name
GetName () ==
return name;
pure public GetAddress : () ==> Address
GetAddress() ==
return address;
end Cardholder
Clock.vdmpp
class Clock
types
public Date = seq of char;
instance variables
date : Date := [];
operations
public SetDate : Date ==> ()
SetDate(d) ==
date := d;
pure public GetDate : () ==> Date
GetDate() ==
return date;
end Clock