Formal Modelling for Systems of Systems
Author: Peter Gorm Larsen and Alvaro Miyazawa and Jim Woodcock
This is the library example which originally was posed in the early 1980’s and a study of 12 specifications of the problem was examined in: “A Study of 12 Specifications of the Library Problem” by Jeanette Wing, July 1988 in IEEE Software. In this model a VDM part was introduced by Peter Gorm Larsen and the reactive part was added by Alvaro Miyazawa and Jim Woodcock. The core of this model illustrate the use of most of the CML data types. The way guards in the reactive parts are made illustrate how to reach deadlock situations using the CML debugger.
types
Command = Borrow | Renew | Return | Find
String = seq of char
BookId = token
UserId = token
BorrowMap = map UserId to set of BookId
Book ::
title : String
author : String
User ::
name : String
Borrow ::
copy : BookId
user : UserId
Renew ::
copy : BookId
user : UserId
Return :: copy : BookId
Find :: string : String
Library ::
books : map BookId to Book
users : map UserId to User
borrowed : BorrowMap
inv mk_Library(bs,us,bor) ==
dom bor subset dom us
and dunion rng bor subset dom bs
and (forall u1, u2 in set dom bor @ u1 <> u2 => bor(u1) inter bor(u2) = {})
values
user1 = mk_User("User1")
user2 = mk_User("User2")
book1 = mk_Book("Book1", "Author1")
book2 = mk_Book("Book2", "Author2")
users = {mk_token(user1) |-> user1, mk_token(user2) |-> user2}
books = {mk_token(book1) |-> book1, mk_token(book2) |-> book2}
functions
ExeBorrow: Borrow * Library -> Library
ExeBorrow(b,l) ==
mk_Library(l.books,
l.users,
l.borrowed++{b.user |-> BorrowCopy(b.user,b.copy,l.borrowed)})
pre
b.copy in set dom l.books
and b.user in set dom l.users
and b.copy not in set dunion rng l.borrowed
BorrowCopy: UserId * BookId * BorrowMap -> (set of BookId)
BorrowCopy(u,c,bor) ==
if u in set dom bor
then bor(u) union {c}
else {c}
ExeReturn: Return * Library -> Library
ExeReturn(r, l) ==
mk_Library(l.books,l.users,RemoveCopy(r.copy,l.borrowed))
pre r.copy in set dom l.books
RemoveCopy: BookId * BorrowMap -> BorrowMap
RemoveCopy(c,bor) ==
{u |-> bor(u) \ {c} | u in set dom bor}
ExeFind: String * Library -> (set of BookId)
ExeFind(s,l) ==
{bid | bid in set dom l.books @ s in set {l.books(bid).title, l.books(bid).author}}
pre card({bid | bid in set dom l.books @
s in set {l.books(bid).title, l.books(bid).author}}) > 0
channels
borrow: Borrow
retBook: Return
renew: Renew
loans: UserId*nat
find:Find
process LibraryProcess = begin
state
library: Library := mk_Library({|->},{|->},{|->})
booksP : set of BookId := {}
inv
(dom(library.borrowed) = dom(library.users)) and
(dunion rng(library.borrowed) subset dom(library.books))
functions
GetBorrowed: Library -> BorrowMap
GetBorrowed(l) == l.borrowed
ApplyBorrowed: Library*UserId -> set of BookId
ApplyBorrowed(l,u) == (GetBorrowed(l))(u)
operations
Init: map BookId to Book * map UserId to User ==> ()
Init(bs, us) ==
(library := mk_Library(bs,us,{u|->{}| u in set dom us});
booksP := {})
actions
Act =
(
borrow?b -> [pre_ExeBorrow(b,library)] & (library := ExeBorrow(b,library))
[]
renew?r -> [pre_ExeReturn(mk_Return(r.copy),library)] &
(library := ExeReturn(mk_Return(r.copy),library);
library := ExeBorrow(mk_Borrow(r.copy,r.user),library))
[]
retBook?r1 -> [pre_ExeReturn(mk_Return(r1.copy),library)] & (library := ExeReturn(mk_Return(r1.copy),library))
[]
find?f -> (booksP := ExeFind(f.string,library))
[]
loans?u!(card(ApplyBorrowed(library,u))) -> [ (u in set dom(GetBorrowed(library))) ] & Skip
); Act
@
Init(books,users); Act
end