Introduction to VDM2, Simple AST extensions and
Concurrency in VDM++
Professor Peter Gorm Larsen
([email protected])
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
1
Agenda
Administrative information about the course
• Simple AST Extensions
• Concurrency primitives in VDM++
• Example: POP3 Server
• Example: MSAWConc
• Concurrency and Overture
• Feedback on abstraction test and VDM1 reports
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
2
Teaching Material
• John Fitzgerald, Peter Gorm Larsen, Paul
Mukherjee, Nico Plat and Marcel Verhoef:
Validated Designs for Object-oriented Systems.
Springer Verlag, 2005. (second part)
• Development Process of Distributed Embedded
Systems using VDM, Peter Gorm Larsen et al,
2010.
• The Overture tool (v0.2) used during the course
• Enterprise Architect
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
3
TIVDM2 web pages
• All information concerning this course including
lecture notes, assignments announcements, etc. can
be found on the TIVDM2 web pages
http://kurser.iha.dk/eit/tivdm2/
• You should check this site frequently for new
information and changes. It will be your main source
of information for this unit. The layout of the
WebPages should be fairly self explanatory
• Campus WebPages will be used only for mailing
information
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
4
Education Form
• Confrontation with the teacher
• Thursdays 8:00 – 16:00 in Room 316
• Read in advance of each lecture
• Combination of
• Lessons teaching theory
• Strategy for lessons: quick intro to concepts and then usage in
larger examples
• Continuation of projects where theory is turned into practice
• Using Overture for projects
• Exam form
• 15 minutes oral examination without preparation + 5 minutes for
evaluation
• Oral examination will be centered around projects performed
• Projects reused from TIVDM1 and extended further
• Exam will be on the 10th of June 2010
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
5
Learning Objectives
The participants must at the end of the course be able to:
• Discuss and compare different abstract models
(sequential, concurrent and distributed) in relation to each
other.
• Explain constructs and concepts in the concurrent, realtime and distributed part of the modelling language
VDM++.
• Define and explain syntax and semantics for the
concurrent, real-time and distributed subset of VDM++.
• Apply VDM++ and UML with the associated tool support
for either the description of semantics of a programming
language or for abstract and precise modelling and
validation of concurrent, real-time and distributed systems.
• Evaluate practical use of VDM++ for the validation of
concrete distributed and embedded systems.
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
6
Evaluation principles
• The project reports will be evaluated against:
• Mastering abstraction
• Testability of the VDM++ models
• Use of basic VDM++ structures
• Use of VDM++ concurrency principles (for RT projects)
• Use of VDM++ real-time primitives (for RT projects)
• Exploration of alternative distributive architectures (RT)
• Using VDM for prog lang semantics issues (for AST projects)
• VDM++/UML model quality considerations
• Refection of pros and cons with the VDM-RT approach (RT)
• Report quality including the use of logfile analysis (RT)
• The exam will be evaluated against:
• The project report
• The project presentation by the student
• The students ability to show understanding of VDM++/UML
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
7
Focus in this course
• Focus is on
• Abstract modeling of realistic systems
• Understanding the VDM concepts for AST handling,
concurrency, real-time and distribution
• Learning how to read models made in VDM++/UML
• Learning how to write models in VDM++/UML
• Learning how to move from a sequential model, via a
concurrent model to a real-time distributed model
• Learning how to validate all these models
• Focus is not on
• Toy examples
• Implementation
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
8
Why have this course?
• To understand the underlying primitives for being able to
model complex concurrent and distributed computer
systems
• To understand how language semantics can be
described using VDM++ concepts
• To be able to comprehend the formulation of important
desirable properties precisely
• To be able to express important desirable properties
(including real-time) precisely
• To enable the formulation of abstract models in an
industrially applicable formal notation
• To validate those models to increase confidence in their
correctness and eliminate potential architectural
bottlenecks
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
9
Structure of the course
Week
1. Introduction, Concurrency in VDM++, AST simple
extensions (chap 12)
2. Real-time and distributed modelling in VDM++
(additional notes)
3. Model Quality (chap 13)
4. More about semantics about different language
constructs in VDM++
5. Model Structuring and Combining Views (chap 9+10)
6. Report writing
7. Course evaluation and repetition (if desired)
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
10
Anticipated Plan with Projects
• Week 1: Revisit the model from TIVDM1
• Week 2: Add concurrency to the model and validate it
• Week 3: Add real-time and distribution to the model +
Present initial ideas and get feedback on distributed
real-time models. Validate the model and experiment
with alternative distribution architectures
• Week 4: Work on your project
• Week 5: Present final distributed real-time models
• Week 6: Write report for the project
• Week 7: Project report is handed in to the teacher.
Evaluation of insight gained by using the VDM-RT
extensions to VDM++
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
11
Agenda
Administrative information about the course
Simple AST Extensions
• Concurrency primitives in VDM++
• Example: POP3 Server
• Example: MSAWConc
• Concurrency and Overture
• Feedback on abstraction test and VDM1 reports
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
12
Extensions of Simple
• Introduction of operations
•
•
•
•
Notion of state
Block statements
Assignment statements
Operation calls and return statements
• Introduction of set expressions
• Both enumeration and comprehensions
• Also set type in type system
• Introduction of higher-order functions
• Functions that yield functions as results
• Typically used in functional programming languages
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
13
Introduction of operations
• Notion of state:
• <state definition> ::= <identifier> ":" <type> ":=" <expression>
• Operation definition:
• <operation definition> ::=
<identifier> <paramlist> "==" <statement>
• Statements:
• <statement> = <block statement> |<assignment statement> |
<call statement> | <return statement>
• <block statement> ::= <statement> | "(" [ { <statement> } ] ")"
• <assignment statement> ::= <identifier> ":=" <expression>
• <call statement> ::=
• <identifier> "(" [ <expression> {"," <expression>} ] ")"
• <return statement> ::= "return" <expression>
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
14
Introduction of set expressions
• Set enumerations:
• <set enumeration> ::=
"{" [ <expression> ] {"," <expression> } "}"
• Set Comprehensions:
• <set comprehension> ::=
"{" <expression>
"|" <identifier> "in set" <expression>
"&" <expression> "}”
• Set types:
• <type> ::= "real" | "int" | "nat" | "bool" | "set of" <type> |
<identifier>
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
15
Introduction of
higher-order functions
• Higher order functions:
• <function definition> ::=
<identifier> <paramlist> { <paramlist> } "=="
<expression>
• Parameter lists:
• <paramlist> ::= "(" <parameter> {"," <parameter>} ")"
• Example of a higher order function:
• Add(x : int)(y : int) == x + y
• Here ”Add(7)” is similar to a new function like:
• lambda y : int & 7 + y
• Which is a new function that can be passed around as an
argument or called with other arguments
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
16
Agenda
Administrative information about the course
Simple AST Extensions
Concurrency primitives in VDM++
• Example: POP3 Server
• Example: MSAWConc
• Concurrency and Overture
• Feedback on abstraction test and VDM1 reports
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
17
Concurrency Primitives in VDM++
• Concurrency in VDM++ is based on threads
• Threads communicate using shared objects
• Synchronization on shared objects is specified using
permission predicates
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
18
Threads
• Modelled by a class with a thread section
class SimpleThread
thread
IO`print(”Hello World”)
end SimpleThread
• Thread execution begins using start statement
with an instance of a class with a thread
definition
start(new SimpleThread())
• Note that execution ends when debug thread
is finished
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
19
Thread Communication
• Threads operating in isolation have limited use.
• In VDM++ threads communicate using shared
objects.
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
20
A Producer-Consumer Example
•
•
•
•
•
Concurrent threads must be synchronized
Illustrate with a producer-consumer example
Produce before consumption …
Assume a single producer and a single consumer
Producer has a thread which repeatedly places data
in a buffer
• Consumer has a thread which repeatedly fetches data
from a buffer
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
21
The Producer Class
class Producer
instance variables
b : Buffer
operations
Produce: () ==> seq of char
Produce() == ...
thread
while true do
b.Put(Produce())
end Producer
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
22
The Consumer Class
class Consumer
instance variables
b : Buffer
operations
Consume: seq of char ==> ()
Consume(d) == ...
thread
while true do
Consume(b.Get())
end Consumer
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
23
The Buffer Class
class Buffer
instance variables
data : [seq of char] := nil
operations
public Put: seq of char ==> ()
Put(newData) ==
data := newData;
public Get: () ==> seq of char
Get() ==
let oldData = data
in
( data := nil;
return oldData
)
end Buffer
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
24
Permission Predicates
• What if the producer thread generates values
faster than the consumer thread can consume
them?
• Shared objects require synchronization.
• Synchronization is achieved in VDM++ using
permission predicates.
• A permission predicate describes when an
operation call may be executed.
• If a permission predicate is not satisfied, the
operation call blocks.
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
25
Permission Predicates
• Permission predicates are described in the sync
section of a class
sync
per <operation name> => predicate
• The predicate may refer to the class’s instance
variables.
• The predicate may also refer to special variables
known as history counters.
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
26
History Counters
Counter
Description
#req op
The number of times that op has been requested
#act op
The number of times that op has been activated
#fin op
The number of times that op has been completed
#active op
The number of active executions of op
#waiting op The number of waiting executions of op
#active op = #act op - #fin op
#waiting op = #req op - #act op
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
27
The Buffer Synchronized
• Assuming the buffer does not lose data, there are two
requirements:
• It should only be possible to get data, when the
producer has placed data in the buffer.
• It should only be possible to put data when the
consumer has fetched data from the buffer.
• The following permission predicates could model
these requirements:
• per Put => data = nil
• per Get => data <> nil
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
28
The Buffer Synchronized (2)
• The previous predicates could also have been written
using history counters:
• For example
per Get => #fin(Put) - #fin(Get) = 1
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
29
Mutual Exclusion
• Another problem could arise with the buffer: what if
the producer produces and the consumer consumes
at the same time?
• The result could be non-deterministic and/or counterintuitive.
• VDM++ provides the keyword mutex
• mutex(Put, Get)
• Shorthand for
• per Put => #active(Get) = 0
• per Get => #active(Put) = 0
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
30
Agenda
Administrative information about the course
Simple AST Extensions
Concurrency primitives in VDM++
Example: POP3 Server
• Example: MSAWConc
• Concurrency and Overture
• Feedback on abstraction test and VDM1 reports
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
31
Example: POP3 Server
• Protocol which allows email clients to fetch messages
from a server.
• Server contains a collection of messages for a
number of users.
• Server is typically capable of communicating with
multiple clients concurrently.
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
32
Overall Class Structure
POP3Server
POP3ClientHandler
-parent
-connChannel
-msgChannel
MessageChannelBuffer
TIVDM2
0..1
-data
Introduction, AST extensions and Concurrency
in VDM++
MessageChannel
33
Behaviour
• The server listens constantly for clients.
• When a client initiates contact, a client handler is
spawned.
• The client handler then responds to commands from
the client, until the client terminates the session.
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
34
The POP3Server
Instance Variables
class POP3Server
instance variables
maildrop
: MailDrop;
passwords
: map POP3Types`UserName to POP3Types`Password;
locks
: map ClientHandlerId to POP3Types`UserName;
serverStarted : bool := false;
types
public MailDrop = map POP3Types`UserName to MailBox;
public MailBox ::
msgs
: seq of POP3Message
locked : bool;
public ClientHandlerId = nat;
end POP3Server
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
35
The POP3Server
Basic Synchronization
class POP3Server
operations
SetUserMessages: POP3Types`UserName * seq of POP3Message ==> ()
SetUserMessages(user, newMsgs) ==
maildrop(user) := mu(maildrop(user), msgs |-> newMsgs)
pre user in set dom maildrop;
GetUserMail: POP3Types`UserName ==> MailBox
GetUserMail(user) ==
return maildrop(user)
pre user in set dom maildrop;
sync
mutex(SetUserMessages);
mutex(SetUserMessages, GetUserMail)
end POP3Server
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
36
Synchronization of Locking
class POP3Server
operations
public AcquireLock: ClientHandlerId * POP3Types`UserName ==> ()
AcquireLock (clId, user) ==
locks := locks ++ { clId |-> user}
pre clId not in set dom locks;
public ReleaseLock: ClientHandlerId ==> ()
ReleaseLock(clId) ==
locks := {clId} <-: locks
pre clId in set dom locks;
public IsLocked: POP3Types`UserName ==> bool
IsLocked(user) ==
return user in set rng locks;
sync
mutex(AcquireLock);
mutex(ReleaseLock);
mutex(AcquireLock, ReleaseLock, IsLocked);
end POP3Server
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
37
Client Handler States
• Three states:
• Authorisation: The client has not yet been authorised by the
client handler.
• Transaction: The client is able to interrogate the client handler
about the contents of the mail box for the client's user.
• Update:The client has ended the session; messages marked for
deletion are actually deleted from the server, then the thread
dies.
class POP3ClientHandler
ServerState = <Authorization> | <Transaction> | <Update>;
end POP3ClientHandler
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
38
Starting a Client Session
class POP3Server
thread
while true do
( let msgChannel = connChannel.Get()
in
CreateClientHandler(msgChannel);
serverStarted := true;
)
instance variables
connChannel: MessageChannelBuffer;
operations
CreateClientHandler: MessageChannel ==> ()
CreateClientHandler(mc) ==
start(new POP3ClientHandler(self, mc));
end POP3Server
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
39
Interacting with the Client 1
class POP3Types
types
public ClientCommand = StandardClientCommand |
OptionalClientCommand;
public StandardClientCommand = QUIT | STAT | LIST | RETR |
DELE | NOOP | RSET;
public OptionalClientCommand = TOP | UIDL | USER | PASS |
APOP;
public
…
public
public
public
RETR :: messageNumber : nat;
ServerResponse = OkResponse | ErrResponse;
OkResponse :: data : seq of char;
ErrResponse :: data : seq of char;
end POP3Types
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
40
Interacting with the Client 2
class POP3ClientHandler
thread
( dcl cmd: POP3Types`ClientCommand;
id := threadid;
cmd := msgChannel.ServerListen();
while (cmd <> mk_POP3Types`QUIT()) do
( msgChannel.ServerSend(ReceiveCommand(cmd));
cmd := msgChannel.ServerListen()
);
msgChannel.ServerSend(ReceiveCommand(cmd));
)
operations
ReceiveCommand: POP3Types`ClientCommand ==> POP3Types`ServerResponse
ReceiveCommand(c) ==
cases c:
mk_POP3Types`QUIT()
-> ReceiveQUIT(c),
mk_POP3Types`STAT()
-> ReceiveSTAT(c),
mk_POP3Types`LIST(-)
-> ReceiveLIST(c),
mk_POP3Types`RETR(-)
-> ReceiveRETR(c),
mk_POP3Types`DELE(-)
-> ReceiveDELE(c),
mk_POP3Types`NOOP()
-> ReceiveNOOP(c),
mk_POP3Types`RSET()
-> ReceiveRSET(c),
mk_POP3Types`TOP(-,-) -> ReceiveTOP(c),
mk_POP3Types`UIDL(-)
-> ReceiveUIDL(c),
mk_POP3Types`USER(-)
-> ReceiveUSER(c),
mk_POP3Types`PASS(-)
-> ReceivePASS(c)
end
end POP3ClientHandler
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
41
Interacting with the Client 3
class POP3ClientHandler
instance variables
ss
: ServerState;
parent: POP3Server;
user : POP3Types`UserName;
id
: POP3Server`ClientHandlerId;
operations
ReceiveRETR: POP3Types`RETR ==> POP3Types`ServerResponse
ReceiveRETR(retr) ==
if ss = <Transaction>
then if parent.IsValidMessageNumber(user, retr.messageNumber)
then let msgText = parent.GetMessageText(user, retr.messageNumber),
sizeText = int2string(parent.GetMessageSize(user,
retr.messageNumber))
in
return mk_POP3Types`OkResponse(sizeText ^ "\n" ^ msgText)
else return mk_POP3Types`ErrResponse(unknownMessageMsg)
else return mk_POP3Types`ErrResponse(negativeStatusMsg);
end POP3ClientHandler
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
42
Synchronized Communication
in the POP3 Server 1
class MessageChannel
instance variables
data : [POP3Types`ClientCommand | POP3Types`ServerResponse]
:= nil;
operations
Send: POP3Types`ClientCommand | POP3Types`ServerResponse ==> ()
Send(msg) ==
data := msg;
Listen: () ==> POP3Types`ClientCommand | POP3Types`ServerResponse
Listen() ==
let d = data in
( data := nil; return d
);
end MessageChannel
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
43
Synchronized Communication
in the POP3 Server 2
class MessageChannel
operations
public ServerSend: POP3Types`ServerResponse ==> ()
ServerSend(p) ==
Send(p);
public ServerListen: () ==> POP3Types`ClientCommand
ServerListen() ==
Listen();
…
sync
per ClientSend => #fin(ServerSend) = #fin(ClientListen) and
#fin(ClientSend) = #fin(ServerListen) and
#fin(ServerSend) = #fin(ClientSend);
per ServerListen => #fin(ClientSend) - 1 = #fin(ServerListen);
end MessageChannel
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
44
Sequence Diagram
client :
POP3Test
handler :
POP3ClientHandler
buffer :
MessageChannel
ServerListen( )
ClientSend(POP3Types`ClientCommand)
ClientListen( )
ServerSend(POP3Types`ServerResponse)
ServerListen( )
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
45
Agenda
Administrative information about the course
Simple AST Extensions
Concurrency primitives in VDM++
Example: POP3 Server
Example: MSAWConc
• Concurrency and Overture
• Feedback on abstraction test and VDM1 reports
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
46
The TimeStamp Class (1/3)
class TimeStamp
instance variables
currentTime : nat := 0;
wakeUpMap : map nat to nat := {|->};
operations
public WaitRelative : nat ==> ()
WaitRelative(val) ==
AddToWakeUpMap(threadid, currentTime + val);
public WaitAbsolute : nat ==> ()
WaitAbsolute(val) ==
AddToWakeUpMap(threadid, val);
AddToWakeUpMap : nat * nat ==> ()
AddToWakeUpMap(tId, val) ==
wakeUpMap := wakeUpMap ++ { tId |-> val };
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
47
The TimeStamp Class (2/3)
public NotifyThread : nat ==> ()
NotifyThread(tId) ==
wakeUpMap := {tId} <-: wakeUpMap;
public NotifyAll : () ==> ()
NotifyAll() ==
let threadSet : set of nat = {th | th in set dom wakeUpMap
& wakeUpMap(th) <= currentTime }
in
for all t in set threadSet
do
NotifyThread(t);
NotifyAndIncTime : () ==> ()
NotifyAndIncTime() ==
( currentTime := currentTime + 1;
NotifyAll();
);
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
48
The TimeStamp Class (3/3)
public GetTime : () ==> nat
GetTime() ==
return currentTime;
sync
mutex(NotifyAll);
mutex(AddToWakeUpMap);
mutex(AddToWakeUpMap, NotifyAll);
end TimeStamp
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
49
The ClockTick Class
class ClockTick is subclass of GLOBAL
instance variables
tid : int := -1;
operations
public ClockTick : Time ==> ClockTick
ClockTick (t) == tid := t;
thread
while true do
(World`timerRef.NotifyThread(tid);
World`timerRef.WaitRelative(1);
)
end ClockTick
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
50
The World Class
class World
…
public World : () ==> World
World() ==
( env := new Environment("scenario.txt");
env.setAirSpace(MSAW`airspace);
MSAW`atc.addObstacle(MSAW`militaryZone);
MSAW`atc.addRadar(MSAW`radar1);
MSAW`atc.addRadar(MSAW`radar2);
);
public Run : () ==> ()
Run() ==
(start(env);
start(MSAW`atc);
env.isFinished();
MSAW`atc.isFinished();
env.showResult()
)
end World
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
51
The Environment Thread
class Environment
…
thread
(start(new ClockTick(threadid));
while World`timerRef.GetTime() < simtime do
(updateFOs();
if updating
then (World`timerRef.WaitRelative(0);
updating := false);
World`timerRef.NotifyAndIncTime();
World`timerRef.Awake();
);
busy := false;
)
end Environment
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
52
The Environment Synchronisation
class Environment
...
public isFinished : () ==> ()
isFinished() == skip;
sync
mutex(handleFOWarningEvent);
per isFinished => not busy;
mutex(handleRadarWarningEvent);
mutex(handleRadarWarningEvent,
handleFOWarningEvent);
end Environment
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
53
Air Traffic Controller (1/2)
class AirTrafficController is subclass of GLOBAL
...
operations
public isFinished : () ==> ()
isFinished() ==
for all r in set radars do
r.isFinished();
public Step : () ==> ()
Step() ==
( for all r in set radars
do
r.Scan(MSAW`airspace);
updateHistory();
findThreats();
busy := false
);
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
54
Air Traffic Controller (2/2)
thread
(for all r in set radars do
start(r);
while true do
Step();
)
sync
per isFinished => not busy;
per Step => busy
end AirTrafficController
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
55
The Radar Class Thread & Sync
class Radar
...
thread
while true do
(let as = MSAW`airspace
in
(detected := { x.getId() |-> x | x in set as.getAirspace() & InRange(x)};
UpdatePriorityList();
World`timerRef.WaitRelative(TimeStamp`stepLength);
World`timerRef.NotifyAll();
World`timerRef.Awake();
)
)
sync
per isFinished => not busy;
mutex(removeNotDetected);
mutex(addNewlyDetected);
mutex(UpdatePriorityList)
end Radar
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
56
Agenda
Administrative information about the course
Simple AST Extensions
Concurrency primitives in VDM++
Example: POP3 Server
Example: MSAWConc
Concurrency and Overture
• Feedback on abstraction test and VDM1 reports
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
57
Concurrency and Overture
• Overture provides
•
•
•
•
Type checking of thread and sync sections of a class.
Interpretation of threads in a deterministic fashion.
All threads are stopped when a breakpoint is reached.
Threadid and information for the broken thread can be
inspected in the debug perspective.
• Note that the scheduler for concurrency is VERY new
• VDMTools additionally provide code generation of
thread and sync sections of a class (Java only).
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
58
Agenda
Administrative information about the course
Simple AST Extensions
Concurrency primitives in VDM++
Example: POP3 Server
Example: MSAWConc
Concurrency and Overture
Feedback on abstraction test and VDM1 reports
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
59
Answers for the Libary questions
•
•
•
•
•
•
•
TIVDM2
On the basis of your understanding of the text, which of the following
statements do you agree with?
• Multiple copies can exist for the same book
Do the requirements say anything about the order used for transaction 3?
• No
Can an ordinary borrower return a book?
• Yes, if he delegates it to a staff user
Can new users be added to the library?
• Not clear from the text
Can staff users also be ordinary borrowers?
• Not clear from the text
Is there a limit for how many books a staff user may borrow?
• No
What information can we deduce from the text that we need to record for
a book? (check all that apply)
• Author
• Subject
• Copies of it
Introduction, AST extensions and Concurrency
in VDM++
60
Answers for the
Student questions
•
On the basis of your understanding of the text, which of the following statements
do you agree with?
•
•
Do the requirements say anything about the order in the list of courses used for
function 3?
•
•
No
What information can we deduce from the text that we need to have for a course or
course occurrence?
•
•
•
•
TIVDM2
Not clear from the text
Is there a limit on how many enrolments a student may have overall?
•
•
Not clear from the text
Can staff users also be students?
•
•
Yes, if it is done with the help of a staff user
Can new students be added to the system?
•
•
No
Can an ordinary student enrol in a course?
•
•
Multiple occurrences of “course occurrences” can exist of the same “course”
Teacher(s)
Title
Study program
State of a course
Introduction, AST extensions and Concurrency
in VDM++
61
Student performances
Leni Lausdahl
Michael Mortensen
José Esparza
Morten Mikkelsen
Johannes Jensen
Hans Chr Jørgensen
Jon Nielsen
Allan Kristensen
Jeppe Sørensen
Lasse Rasmussen
Frederik Laulund
Christian Jensen
Kim Bjerge
Average
TIVDM2
begin
lib
lib
stud
lib
stud
stud
stud
lib
stud
lib
lib
stud
lib
end
stud
stud
lib
stud
lib
lib
lib
stud
lib
stud
stud
lib
stud
begin
end
change
5.166667
4.75 -0.416667
6.166667
9.5 3.333333
5.5
11.5
6
8.666667
5.75 -2.916667
9.25
6.5
-2.75
4.5
8.25
3.75
4.25
6.75
2.5
8.75
10.5
1.75
6.416667
8 1.583333
6
10
4
7.166667
7.75 0.583333
4
6.667
2.667
7.5
6.5
-1
5.555556
Introduction, AST extensions and Concurrency
in VDM++
6.8278 1.272244
62
Summary
• What have I presented today?
•
•
•
•
•
•
Administrative information about the course
Simple Extensions
Concurrency primitives in VDM++
The POP3 and MSAW Concur examples
Concurrency support in Overture
Feedback on abstraction test and VDM1 reports
• What do you need to do now?
• Inspect the electronic copy of the POP3 example
• Get new version of Overture installed and start looking at
the language manual
• Revisit your project
• Present your project selection to all of us
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
63
Quote of the day
It’s different, in that we take on novel tasks every time.
The number of times civil engineers make mistakes is very
small. And at first you think, what’s wrong with us? It’s
because it’s like we’re building the first skyscraper every
time.
Bill Gates
TIVDM2
Introduction, AST extensions and Concurrency
in VDM++
64
Descargar

Defining Data and Functionality