Introduction, Model Structuring and Combining UML and VDM++ Views : Introduction, Model Structuring and Combining UML and VDM++ Views Peter Gorm Larsen
Agenda : Agenda Administrative information about the course
Combining UML and VDM++ Views
The Enigma Cipher Example
Teaching Material : 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 Guidelines for Real-Time Systems Using VDMTools, CSK document, 2006
Tool used during the course http:/www.vdmtools.jp/en
Setup.exe files and documentation can also be found under K:\from eit_staff to eit_stud\PGL
Eclipse with showtrace for graphical views of traces
Rational Rose for UML models to be requested from K:\from eit_staff to eit_stud\PGL
New Extensions to VDM++ : New Extensions to VDM++ Enable the formal description of distributed systems
A result of new research conducted by Marcel Verhoef and Peter Gorm Larsen
Dynamic semantics specified summer 2006 by Peter Gorm Larsen in 567 pages document
Specification test with lots of test cases
Corresponding implementation made by CSK in Japan
New version of development guidelines written summer 2006 by Peter Gorm Larsen
You will be the first external people to read the guidelines and use the new VDMTools VICE executable
Please report all problems you discover so we can fix them
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 web pages
Education Form : Confrontation with the teacher
Wednesdays 8:00 – 11:00 in Room 424
Fridays 13:00 – 15:45 in Room 424
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 VDMTools (new VICE extended version) for projects
Exam form
25 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 4th of January 2007 starting at 8:30 Education Form
Evaluation principles : 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
Use of VDM++ real-time primitives
Exploration of alternative distributive architectures
VDM++/UML model quality considerations
Report quality including the use of trace analysis
The exam will be evaluated against:
The project report
The project presentation by the student
The students ability to show understanding of VDM++/UML
Focus in this course : Focus in this course Focus is on
Abstract modeling of realistic systems
Understanding the VDM concepts for 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
Why have this course? : Why have this course? To understand the underlying primitives for being able to model complex concurrent and distributed computer systems
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
Structure of the course : Structure of the course Week
Model Structuring and Combining Views (chap 9+10)
Concurrency in VDM++ (chap 12)
Real-time and distributed modelling in VDM++ (1)
Real-time and distributed modelling in VDM++ (2)
Model Quality (chap 13)
Report writing
Course evaluation and revision
Projects selected in TIVDM1 : Projects selected in TIVDM1 SAFER
Production Cell
Cash Dispenser
CyberRail
Car radio navigation system
Self navigating vehicle
Personal Medical Unit
Reconsider project
Reconsider grouping
Anticipated Plan with Projects : 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
Week 4: Validate the model and experiment with alternative distribution architectures
Week 5: Write report for the project
Week 6: Project report is handed in to the teacher
Week 7: Evaluation of insight gained by using the new VICE extensions to VDM++
Agenda : Agenda Administrative information about the course
Combining UML and VDM++ Views
The Enigma Cipher Example
The CSLaM System : The CSLaM System A small system for control speed limitation and monitoring for trains
The CSLaM Requirements : The CSLaM Requirements The main purpose of the CSLaM system is to provide a continuous train speed monitoring function. This system is intended to be used when temporary speed restrictions are necessary. This is signalled using different types of beacons placed along the track.
The maximum permitted speed is the lower of the maximum speed of which the train is capable and the speed limits imposed by the temporary speed restriction beacons. If the train speed exceeds the maximum permitted speed, various actions are initiated by the train's on-board computer, depending on the severity of the violation. It is ultimately possible for the on-board system to activate the emergency brake automatically if the train's excess speed is too great.
The CSLaM system components are:
the on-board control speed limitation (CSL) subsystem;
the trackside beacons; and
the performance monitoring subsystem.
The On-board CSL System : The On-board CSL System
The CSL Associations : The CSL Associations class CSL
instance variables
cabDisplay : CabDisplay;
emergencyBrake : EmergencyBrake;
onboardComp : OnBoardComp;
end CSL
There is a one-to-one relationship between
classes in UML and classes in VDM++. Mapping rule 1 Every association between two classes at the UML
class diagram level must be given a role name Mapping rule 2
Additional basic mapping rules 1 : Additional basic mapping rules 1 Attributes inside a UML class are represented as instance variables or values inside the corresponding VDM++ class. The stereotype will indicate the kind, and the default will be instance variables. Mapping rule 3: Attributes Operations inside a UML class are represented as functions and
operations in the corresponding VDM++ class, in accordance with the function or operation stereotype, and vice versa. By default the stereotype is operation. Mapping rule 4: Functionality All member declarations can have access modifiers at both the UML class diagram; the VDM++ level and the mapping rules for these are one to one. The only exception here is that implementation at the UML class diagram level is considered as private at the VDM++ level. Mapping rule 5: Access modifiers
Additional basic mapping rules 2 : Additional basic mapping rules 2 Static member declarations at the VDM++ level correspond to static member declarations at the UML class diagram level, except for operations which cannot be declared static inside Rose. Mapping rule 6: Static definitions Type definitions inside a VDM++ class are simply ignored by the mapping rules because there is no equivalent at the UML class diagram level. This just means that type definitions will only be kept at the VDM++ level. Mapping rule 7: Type definitions
The Beacon Classes 1 : The Beacon Classes 1 Announcement Beacon: This announces a limitation beacon. The information provided by the beacon is the target speed that must be respected when the limitation beacon is met. Several announcement beacons might be met successively.
Limitation Beacon: The speed restriction is valid as soon as the head of the train reaches the beacon. If a limitation beacon is not preceded by an announcement beacon, a ground fault is raised.
Cancel Beacon: This beacon cancels all announcements present. If no announcement is available, the cancel beacon is ignored. This beacon is used when a speed restriction is announced before a track switch and is not needed in some branches after the switch.
End Beacon: This ends the speed restriction area. The speed restriction is no longer valid as soon as the tail of the train reaches the end beacon.
The Beacon Classes 2 : The Beacon Classes 2 There is a one-to-one relationship between inheritance
in UML class diagrams and inheritance in VDM++. class AnnounceBeacon is subclass of Beacon
…
end AnnounceBeacon Mapping rule 8: Inheritance
Multiplicity of Associations : Multiplicity of Associations The multiplicity of an association determines its type at the VDM++ level. With
“0..n” multiplicity and an ordered constraint the association is modelled as a sequence of object reference types using the sequence type constructor. Mapping rule 9: Association Multiplicity
Qualified Associations : Qualified Associations class Supervisor
instance variables
driverInfo: map DriverCard to Driver := {|->};
trainInfo : map TrainId to CSL := {|->};
types
public TrainId = token;
end Supervisor Qualified associations use a type (or a class name) as the qualifier and are modelled as a mapping from the qualifier type to the object reference type it is going to (possibly with further multiplicity). Mapping rule 10: Qualified Associations
Monitoring Driver Performance : Monitoring Driver Performance class CSL
instance variables
driverCard: [DriverCard] := nil;
faults : set of Fault := {};
end CSL The multiplicity of an association determines its type at the VDM++ level.
“0 .. n” multiplicity is modelled as an unordered collection of object reference types using the set type constructor. Mapping rule 11: Collection Associations The multiplicity of an association determines its type at the VDM++ level. Unspecified (or with 1) multiplicity is simply modelled as an object reference type. “0 .. 1” multiplicity is modelled as an optional type. Mapping rule 12: Optional Associations
Agenda : Agenda Administrative information about the course
Combining UML and VDM++ Views
The Enigma Cipher Example
The Enigma Cipher : The Enigma Cipher Used by the Germans during the Second World War
Encryption and decryption
Cracked by ”bombes” by the Allies at Bletchley Park
More powerful cypher system cracked by ”Colossus”
Influenced the outcome of the war
Some believe that Alan Turing was involved in the worlds first computer
Basic principles of Encryption : Basic principles of Encryption Around 1400 Leon Alberti invented the cipher disk
Substition of letters in a monalphabetic fashion
Caesar ciphers have an encoding distance
Distance of 4 would make A -> E and B -> F
Alberti invented a polyalpahbetic cipher
Coding distance implemented by a code word e.g. LEON
Now L -> A for the first letter, E -> A for the second letter
Enigma was made of a plugboard, a set of rotors and a reflector
The plugboard replaces letters
The rotors are jointly called a scambler
The reflector is responsible for making it symmetric
The Structure of the Enigma : The Structure of the Enigma
Initial UML Class Diagram : Initial UML Class Diagram
The Revised Enigma UML Model : The Revised Enigma UML Model
The Alphabet Class : The Alphabet Class class Alphabet
instance variables
alph : seq of char := [];
inv AlphabetInv(alph)
functions
AlphabetInv: seq of char -> bool
AlphabetInv (palph) ==
len palph mod 2 = 0 and
card elems palph = len palph
operations
public Alphabet: seq of char ==> Alphabet
Alphabet (pa) == alph := pa
pre AlphabetInv(pa);
public GetChar: nat ==> char
GetChar (pidx) == return alph(pidx)
pre pidx in set inds alph;
public GetIndex: char ==> nat
GetIndex (pch) ==
let pidx in set {i | i in set inds alph
& alph(i) = pch} in
return pidx
pre pch in set elems alph;
public GetIndices: () ==> set of nat
GetIndices () == return inds alph;
public GetSize: () ==> nat
GetSize () == return len alph;
public Shift: nat * nat ==> nat
Shift (pidx, poffset) ==
if pidx + poffset > len alph
then return pidx + poffset - len alph
else return pidx + poffset
pre pidx in set inds alph and
poffset <= len alph;
public Shift: nat ==> nat
Shift (pidx) == Shift(pidx, 1)
end Alphabet
The Component Class : The Component Class class Component
instance variables
protected next : [Component] := nil;
protected alph : Alphabet
operations
public Successors: () ==> set of Component
Successors () ==
if next = nil
then return {self}
else return {self} union next.Successors();
public SetNext: Component ==> ()
SetNext (pcom) == next := pcom
pre next = nil and
self not in set pcom.Successors();
public Substitute: nat ==> nat
Substitute (-) == is subclass responsibility;
public Rotate: () ==> ()
Rotate () == skip;
public Rotate: nat ==> ()
Rotate (-) == skip
end Component
The Configuration Class 1 : The Configuration Class 1 class Configuration is subclass of Component
instance variables
protected config: inmap nat to nat; Plugboard
{2|->3,3|->2} Rotor
{1|->2,2|->1,3|->4,4|->3} Reflector
{1|->2,3|->4}
The Configuration Class 2 : The Configuration Class 2 operations
protected Encode: nat ==> nat
Encode (penc) ==
if penc in set dom config
then return config(penc)
else return penc;
protected Decode: nat ==> nat
Decode (pdec) ==
let invcfg = inverse config in
if pdec in set dom invcfg
then return invcfg(pdec)
else return pdec;
public Substitute: nat ==> nat
Substitute(pidx) ==
return Decode(next.Substitute(Encode(pidx)))
pre next <> nil
end Configuration
The Reflector Class : The Reflector Class class Reflector is subclass of Configuration
instance variables
inv ReflectorInv(next, config, alph)
functions
ReflectorInv: [Component] * inmap nat to nat * Alphabet -> bool
ReflectorInv (pnext, pconfig, palph) ==
pnext = nil and
dom pconfig inter rng pconfig = {} and
dom pconfig union rng pconfig = palph.GetIndices()
operations
public Reflector: nat * Alphabet * inmap nat to nat ==> Reflector
Reflector (psp, pa, pcfg) ==
atomic (alph := pa;
config := {pa.Shift(i, psp-1) |-> pa.Shift(pcfg(i), psp-1)
| i in set dom pcfg})
pre psp in set pa.GetIndices() and
ReflectorInv(next, pcfg, pa);
public Substitute: nat ==> nat
Substitute (pidx) ==
if pidx in set dom config
then Encode(pidx)
else Decode(pidx)
end Reflector
The Rotor Class 1 : The Rotor Class 1 class Rotor is subclass of Configuration
instance variables
latch_pos : nat;
latch_lock : bool := false;
inv RotorInv(latch_pos, config, alph)
functions
RotorInv: nat * inmap nat to nat * Alphabet -> bool
RotorInv (platch_pos, pconfig, palph) ==
let ainds = palph.GetIndices() in
platch_pos in set ainds and
dom pconfig = ainds and
rng pconfig = ainds and
exists x in set dom pconfig & x <> pconfig(x)
operations
public Rotor: nat * nat * Alphabet * inmap nat to nat ==> Rotor
Rotor (psp, plp, pa, pcfg) ==
atomic (latch_pos := pa.Shift(plp,psp-1);
alph := pa;
config := {pa.Shift(i,psp-1) |-> pa.Shift(pcfg(i),psp-1)
| i in set dom pcfg})
pre psp in set pa.GetIndices() and
RotorInv(plp, pcfg, pa);
The Rotor Class 2 : The Rotor Class 2 public Rotate: () ==> ()
Rotate () ==
(-- propagate the rotation to the next component and tell it where our latch position is
next.Rotate(latch_pos);
-- update our own latch position and take the alphabet size into account
if latch_pos = alph.GetSize()
then latch_pos := 1
else latch_pos := latch_pos+1;
-- update the transpositioning relation by shifting all indices one position
config := {alph.Shift(i) |-> alph.Shift(config(i)) | i in set dom config};
-- remember the rotation
latch_lock := true)
pre isofclass(Rotor,next) or isofclass(Reflector,next);
public Rotate: nat ==> ()
Rotate (ppos) ==
-- compare the latch position and the lock
if ppos = latch_pos and not latch_lock
-- perform the actual rotation
then Rotate()
-- otherwise reset the lock
else latch_lock := false
pre ppos in set alph.GetIndices();
end Rotor
The Plugboard Class : The Plugboard Class class Plugboard is subclass of Configuration
instance variables
inv PlugboardInv(config, alph)
functions
PlugboardInv: inmap nat to nat * Alphabet -> bool
PlugboardInv (pconfig, palph) ==
dom pconfig subset palph.GetIndices()
operations
public Plugboard: Alphabet * inmap nat to nat ==> Plugboard
Plugboard (pa, pcfg) ==
atomic (alph := pa;
config := pcfg munion inverse pcfg)
pre dom pcfg inter rng pcfg = {} and
PlugboardInv(pcfg, pa);
public Substitute: nat ==> nat
Substitute (pidx) ==
(next.Rotate();
Configuration`Substitute(pidx))
pre pidx in set alph.GetIndices() and
(isofclass(Rotor,next) or isofclass(Reflector,next))
end Plugboard
Redefining Substitute : Redefining Substitute
The SimpleEnigma Class : The SimpleEnigma Class class SimpleEnigma is subclass of Component
values
refcfg : inmap nat to nat = {1 |-> 3, 2 |-> 4};
rotcfg : inmap nat to nat = {1 |-> 2, 2 |-> 4, 3 |-> 3, 4 |-> 1};
pbcfg : inmap nat to nat = {2 |-> 3}
operations
public SimpleEnigma: () ==> SimpleEnigma
SimpleEnigma () ==
(dcl cp : Component ;
alph := new Alphabet("ABCD");
next := new Reflector(4,alph,refcfg);
cp := new Rotor(3,3,alph,rotcfg);
cp.SetNext(next); next := cp;
cp := new Rotor(2,2,alph,rotcfg);
cp.SetNext(next); next := cp;
cp := new Rotor(1,1,alph,rotcfg);
cp.SetNext(next); next := cp;
cp := new Plugboard(alph,pbcfg);
cp.SetNext(next); next := cp);
public Keystroke : char ==> char
Keystroke (pch) ==
let pidx = alph.GetIndex(pch) in
return alph.GetChar(next.Substitute(pidx))
pre isofclass(Plugboard,next)
end SimpleEnigma
The VDMUnit Framework : The VDMUnit Framework
The TestSuite Class : The TestSuite Class class TestSuite is subclass of Test
instance variables
tests : seq of Test := [];
operations
public Run: () ==> ()
Run () ==
(dcl ntr : TestResult := new TestResult();
Run(ntr);
ntr.Show());
public Run: TestResult ==> ()
Run (result) ==
for test in tests do
test.Run(result);
public AddTest: Test ==> ()
AddTest(test) ==
tests := tests ^ [test];
end TestSuite
The TestCase Class : The TestCase Class class TestCase is subclass of Test
instance variables
name : seq of char
operations
public TestCase: seq of char ==> TestCase
TestCase(nm) == name := nm;
public GetName: () ==> seq of char
GetName () == return name;
protected AssertTrue: bool ==> ()
AssertTrue (pb) ==
if not pb then exit ;
protected AssertFalse: bool ==> ()
AssertFalse (pb) ==
if pb then exit ;
The TestResult Class : The TestResult Class class TestResult
instance variables
failures : seq of TestCase := []
operations
public AddFailure: TestCase ==> ()
AddFailure (ptst) == failures := failures ^ [ptst];
public Print: seq of char ==> ()
Print (pstr) ==
def - = new IO().echo(pstr ^ "\n") in skip;
public Show: () ==> ()
Show () ==
if failures = [] then
Print ("No failures detected")
else
for failure in failures do
Print (failure.GetName() ^ " failed")
end TestResult
Enigma Unit Tests : Enigma Unit Tests
Summary : Summary What have I presented today?
Administrative information about the course
The rules for mappings between VDM++ and UML
Illustrated by a small Control Speed Limitation and Monitoring (CSLaM) example for trains
Illustrated the Enigma example in VDM++
What do you need to do now?
Read chapters 9 and 10 of the book
Get new version of VDMTools installed and start looking at the new language manual
Revisit your project
Quote of the day : Quote of the day Science is a differential equation. Religion is a boundary condition.
Alan Turing
(1912 - 1954)