01 introduction and UML combination

Information about 01 introduction and UML combination

Published on January 4, 2008

Author: UpBeat

Source: authorstream.com

Content

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 <FAILURE>; protected AssertFalse: bool ==> () AssertFalse (pb) == if pb then exit <FAILURE>; 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)

Related presentations


Other presentations created by UpBeat

Making Disciples
17. 06. 2007
0 views

Making Disciples

CVA Final Version 2006
06. 12. 2007
0 views

CVA Final Version 2006

Children Animals
03. 10. 2007
0 views

Children Animals

whole grains
04. 10. 2007
0 views

whole grains

07 peering and te with bgp
07. 10. 2007
0 views

07 peering and te with bgp

climate promoting sd china
12. 10. 2007
0 views

climate promoting sd china

ppt forest policy
27. 11. 2007
0 views

ppt forest policy

ch04dp3
01. 12. 2007
0 views

ch04dp3

Chairman Award 2 Hickok
02. 11. 2007
0 views

Chairman Award 2 Hickok

Nancy Kerrigan
05. 11. 2007
0 views

Nancy Kerrigan

Academia Sinica 05 30 Sep
15. 11. 2007
0 views

Academia Sinica 05 30 Sep

19361
15. 11. 2007
0 views

19361

Possessives Apostrophe
20. 11. 2007
0 views

Possessives Apostrophe

Malaysia
26. 11. 2007
0 views

Malaysia

compliance
19. 12. 2007
0 views

compliance

upload c beatles64 6n22
21. 12. 2007
0 views

upload c beatles64 6n22

Azerbaijan PPT VCMar02
29. 12. 2007
0 views

Azerbaijan PPT VCMar02

final mccc yougov report
30. 12. 2007
0 views

final mccc yougov report

MikeWhiteDDDMDec1106
05. 11. 2007
0 views

MikeWhiteDDDMDec1106

OpenMPI OpenIB
03. 01. 2008
0 views

OpenMPI OpenIB

what is AI
05. 01. 2008
0 views

what is AI

Basic Plant Physiology
07. 01. 2008
0 views

Basic Plant Physiology

blm doe levy
07. 01. 2008
0 views

blm doe levy

Hedley
12. 11. 2007
0 views

Hedley

AC004
31. 12. 2007
0 views

AC004

ravi keynote
11. 10. 2007
0 views

ravi keynote

globalisation 2008
24. 02. 2008
0 views

globalisation 2008

19741
06. 03. 2008
0 views

19741

james rigney
21. 03. 2008
0 views

james rigney

ShipToAverage
07. 11. 2007
0 views

ShipToAverage

World Indigo Market Monkeys
27. 03. 2008
0 views

World Indigo Market Monkeys

ch09 1
28. 12. 2007
0 views

ch09 1

1992 stations cross esquivel
07. 04. 2008
0 views

1992 stations cross esquivel

A105 017 Blackholes
28. 11. 2007
0 views

A105 017 Blackholes

laurence millar
28. 03. 2008
0 views

laurence millar

lule
09. 04. 2008
0 views

lule

no5
10. 04. 2008
0 views

no5

Energy Scenarios
13. 04. 2008
0 views

Energy Scenarios

disnqmwrqn5ghio
17. 04. 2008
0 views

disnqmwrqn5ghio

Kids Landscape2004
22. 04. 2008
0 views

Kids Landscape2004

46 DNT Japan Tsuji
09. 10. 2007
0 views

46 DNT Japan Tsuji

EPUK presentation FINAL
16. 11. 2007
0 views

EPUK presentation FINAL

adetajan2007
13. 12. 2007
0 views

adetajan2007

ENCHANTED DOLLS
02. 10. 2007
0 views

ENCHANTED DOLLS

nclb overview
28. 11. 2007
0 views

nclb overview

180 07 lec9
16. 11. 2007
0 views

180 07 lec9

china standards retro
12. 10. 2007
0 views

china standards retro

Chapter 20 Outline
11. 12. 2007
0 views

Chapter 20 Outline

2004SellingInChina JamesColony
10. 10. 2007
0 views

2004SellingInChina JamesColony

Psychology and Political Thought
07. 01. 2008
0 views

Psychology and Political Thought

Love 2
17. 06. 2007
0 views

Love 2

Love 1
17. 06. 2007
0 views

Love 1

Love Your Body
17. 06. 2007
0 views

Love Your Body

Love Story Slides 4 Eric
17. 06. 2007
0 views

Love Story Slides 4 Eric

love not leave
17. 06. 2007
0 views

love not leave

Love Dynamics
17. 06. 2007
0 views

Love Dynamics

love eco
17. 06. 2007
0 views

love eco

Medieval lyrics
17. 06. 2007
0 views

Medieval lyrics

MDA USC 2007
17. 06. 2007
0 views

MDA USC 2007

MDA AAAI 2004
17. 06. 2007
0 views

MDA AAAI 2004

Lucy AM
17. 06. 2007
0 views

Lucy AM

lemonade 8
10. 10. 2007
0 views

lemonade 8

esslli07 3
22. 11. 2007
0 views

esslli07 3

BNLTRIP LArTPC Bock
08. 11. 2007
0 views

BNLTRIP LArTPC Bock

Love Your Body2
17. 06. 2007
0 views

Love Your Body2

Lucy PM
17. 06. 2007
0 views

Lucy PM

Season change1
02. 11. 2007
0 views

Season change1

prÃsentationecole
05. 11. 2007
0 views

prÃsentationecole

marcenasjourney
05. 11. 2007
0 views

marcenasjourney

Nets1
28. 12. 2007
0 views

Nets1

SPS Search MSDN evening 030604
12. 12. 2007
0 views

SPS Search MSDN evening 030604

From Crayon to Mouse
18. 12. 2007
0 views

From Crayon to Mouse

The Presentation
14. 03. 2008
0 views

The Presentation

ev
21. 11. 2007
0 views

ev

trt02 eccles
05. 11. 2007
0 views

trt02 eccles

Digging Dinos
12. 09. 2007
0 views

Digging Dinos