Transcription
22c181:Formal Methods in Software EngineeringThe University of IowaSpring 2008Introduction to UMLCopyright 2007-8 Reiner Hähnle and Cesare Tinelli.Notes originally developed by Reiner Hähnle at Chalmers University and modified by Cesare Tinelli at the University of Iowa. These notesare copyrighted materials and may not be used in other course settings outside of the University of Iowa in their current form or modifiedform without the express written permission of one of the copyright holders.22c181: Formal Methods in Software Engineering – p.1/33
ContentsOverview of KeYUML and its semanticsIntroduction to OCLSpecifying requirements with OCLModelling of Systems with Formal SemanticsPropositional & First-order logic, sequent calculusOCL to Logic, horizontal proof obligations, using KeYDynamic logic, proving program correctnessJava Card DLVertical proof obligations, using KeYWrap-up, trends22c181: Formal Methods in Software Engineering – p.2/33
Building Models22c181: Formal Methods in Software Engineering – p.3/33
UMLUnified Modeling LanguageUnified: end to many similar approaches.Booch, Rumbaugh, JacobssonStandardised by OMG (now version 2.0 in finalisation)22c181: Formal Methods in Software Engineering – p.4/33
UMLUnified Modeling LanguageUnified: end to many similar approaches.Booch, Rumbaugh, JacobssonStandardised by OMG (now version 2.0 in finalisation)Modeling: main (creative) process of software developmentTrend in SWE: emphasis on model, MDA/MDECode abstraction, formal model22c181: Formal Methods in Software Engineering – p.4/33
UMLUnified Modeling LanguageUnified: end to many similar approaches.Booch, Rumbaugh, JacobssonStandardised by OMG (now version 2.0 in finalisation)Modeling: main (creative) process of software developmentTrend in SWE: emphasis on model, MDA/MDECode abstraction, formal modelLanguage: Provides notation, no method, no processGraphical, collection of different diagram types22c181: Formal Methods in Software Engineering – p.4/33
UML DiagramsStructural DiagramsBehavioural Diagrams22c181: Formal Methods in Software Engineering – p.5/33
UML DiagramsStructural DiagramsBehavioural Diagrams Class Diagrams Component Diagrams Composite StructureDiagrams Object Diagrams Deployment Diagrams Package Diagrams22c181: Formal Methods in Software Engineering – p.5/33
UML DiagramsStructural DiagramsBehavioural Diagrams Class Diagrams Component Diagrams Composite StructureDiagrams Object Diagrams Deployment Diagrams Package Diagrams22c181: Formal Methods in Software Engineering – p.5/33
UML DiagramsStructural DiagramsBehavioural Diagrams Class Diagrams Component Diagrams Composite StructureDiagrams Object Diagrams Deployment Diagrams Package Diagrams22c181: Formal Methods in Software Engineering – p.5/33
UML DiagramsStructural DiagramsBehavioural Diagrams Class Diagrams Activity Diagrams Component Diagrams Interaction Diagrams Composite StructureDiagrams Sequence Diagrams Collaboration Diagrams. Object Diagrams Deployment Diagrams Package Diagrams Use Case Diagrams State Machine Diagrams22c181: Formal Methods in Software Engineering – p.5/33
UML DiagramsStructural DiagramsBehavioural Diagrams Class Diagrams Activity Diagrams Component Diagrams Interaction Diagrams Composite StructureDiagrams Sequence Diagrams Collaboration Diagrams. Object Diagrams Deployment Diagrams Package Diagrams Use Case Diagrams State Machine Diagrams22c181: Formal Methods in Software Engineering – p.5/33
UML DiagramsStructural DiagramsBehavioural Diagrams Class Diagrams Activity Diagrams Component Diagrams Interaction Diagrams Composite StructureDiagrams Sequence Diagrams Collaboration Diagrams. Object Diagrams Deployment Diagrams Package Diagrams Use Case Diagrams State Machine Diagrams22c181: Formal Methods in Software Engineering – p.5/33
Class DiagramsModel static design view, define vocabulary (signature)ClassCollection of similar objects in a ge-mail:StringstartWork(t:Time)22c181: Formal Methods in Software Engineering – p.6/33
Class DiagramsModel static design view, define vocabulary (signature)ClassCollection of similar objects in a ge-mail:StringstartWork(t:Time)AssociationRelation between classesRelates pairs of class instancesPerson1repairsmechanic0.*Car22c181: Formal Methods in Software Engineering – p.6/33
Class DiagramsModel static design view, define vocabulary (signature)ClassCollection of similar objects in a ge-mail:StringstartWork(t:Time)AssociationRelation between classesRelates pairs of class tionship between classesSportsCarVan22c181: Formal Methods in Software Engineering – p.6/33
Classesclass namename compartmentPersonname:Stringe-mail:Stringattribute namesattribute compartmentattribute types22c181: Formal Methods in Software Engineering – p.7/33
Classesclass namename compartmentPersonname:Stringe-mail:Stringattribute namesattribute compartmentattribute types(J AVA) Semantics of ClassesFor class C let I(C) 6 be set of objects“The objects that can have static type C”22c181: Formal Methods in Software Engineering – p.7/33
The Null TypeNull22c181: Formal Methods in Software Engineering – p.8/33
The Null TypeNullSemantics of NullEach class diagram contains implicitly the Null classNo attributes, no operationsI(Null) {null}null I(C) for any class C“null is typeable with any type C ”22c181: Formal Methods in Software Engineering – p.8/33
ralizationLongPaper22c181: Formal Methods in Software Engineering – p.9/33
ralizationLongPaperSemantics of Subclassessubclass relation: I(ShortPaper) I(Paper)constraint: I(ShortPaper) I(LongPaper) {null}22c181: Formal Methods in Software Engineering – p.9/33
Attributesclass namename compartmentPersonname:Stringe-mail:Stringattribute namesattribute compartmentattribute types22c181: Formal Methods in Software Engineering – p.10/33
Attributesname compartmentPersonclass namename:Stringe-mail:Stringattribute namesattribute compartmentattribute typesSemantics of AttributesI(name) is function from I(Person) to I(String)I(name)(aP erson) gives a string or nullAlways f (null) null22c181: Formal Methods in Software Engineering – p.10/33
Class (Static) lnumber:Integer22c181: Formal Methods in Software Engineering – p.11/33
Class (Static) lnumber:IntegerSemanticsI(totalnumber) is an element of (not a function to) I(Integer)(i.e., Paper.totalnumber is a constant)22c181: Formal Methods in Software Engineering – p.11/33
MultiplicitiesSemanticsMI(M )0.1{0, 1}0. N N1.3{1, 2, 3}7{7}15.19{15, 16, 17, 18, 19}1.3, 7, 15.19{1, 2, 3, 7, 15, 16, 17, 18, 19}(i.e., the separator "," acts as set theoretic union)22c181: Formal Methods in Software Engineering – p.12/33
String3refereerole tion name22c181: Formal Methods in Software Engineering – p.13/33
String3refereerole tion nameSemanticsI(review) is a relation between I(Person)\{null} and I(Paper)\{null}Multiplicity 3 requires: for all pap I(Paper),card({pers I(Person) review(pers, pap)}) 322c181: Formal Methods in Software Engineering – p.13/33
Role Names (Directed :String3refereerole namePaper*review {ordered} authors[*]:Personnumber:Integerassociation nameproperty is ordered22c181: Formal Methods in Software Engineering – p.14/33
Role Names (Directed :String3refereerole namePaper*review {ordered} authors[*]:Personnumber:Integerassociation nameproperty is orderedSemanticsClientSupplierz } {z } {I(referee) : I(Paper) Set(I(Person))(supplier multiplicity 6 1)I(paper) : I(Person) Sequence(I(Paper)) (default role name client)22c181: Formal Methods in Software Engineering – p.14/33
Role Names ng3refereerole namePaper*review {ordered} authors[*]:Personnumber:Integerassociation nameproperty is orderedSemantics of role names compatible with association semanticsI(referee)(aP aper) {aP erson haP erson, aP aperi I(review)}22c181: Formal Methods in Software Engineering – p.15/33
SnapshotsA snapshot of a given class diagram D is a particular semantics I of DUML object diagram (for D) including for each class C: objects I(C) typeable with C maps I(a) : I(C) I(C′ ) for all attributes a of type C′ in class C association instances (pairs) in I(C)\{null} I(C′ )\{null}an interpretation for operations/methods (Java: independent ofsnapshot)(standard) interpretation of predefined primitive data types and theiroperations (Integer, String, . . . )22c181: Formal Methods in Software Engineering – p.16/33
SnapshotsA snapshot of a given class diagram D is a particular semantics I of DUML object diagram (for D) including for each class C: objects I(C) typeable with C maps I(a) : I(C) I(C′ ) for all attributes a of type C′ in class C association instances (pairs) in I(C)\{null} I(C′ )\{null}an interpretation for operations/methods (Java: independent ofsnapshot)(standard) interpretation of predefined primitive data types and theiroperations (Integer, String, . . . )Multiplicities and constraints restrict set of admissiblesnapshots22c181: Formal Methodsin Software Engineering – p.16/33
Object Diagram: (Static Part of) iewid0815:Personname ‘‘Jane’’e-mail erid333:Paperauthors {id0815}number 17reviewid0825:Personname ‘‘Paul’’e-mail ‘‘paul’’reviewid301:Paperauthors {id0815,id0825}number 33Non-admissible (and unintended) instance — Why?22c181: Formal Methods in Software Engineering – p.17/33
Object Diagram: (Static Part of) iewid0815:Personname ‘‘Jane’’e-mail erid333:Paperauthors {id0815}number 17reviewid0825:Personname ‘‘Paul’’e-mail ‘‘paul’’reviewid301:Paperauthors {id0815,id0825}number 33Non-admissible (and unintended) instance — Why?How to exclude that the author of a paper is its own reviewer?22c181: Formal Methods in Software Engineering – p.17/33
Operations: e()getNumber():Integer{query}class nameattributesoperationname & signature22c181: Formal Methods in Software Engineering – p.18/33
Operations: QueriesPaperclass mber():Integer{query}attributesoperationname & signatureSemantics of queries (side-effect free operations, aka pure methods)Function from owner and parameter classes to result classOwnerz } {I(getNumber()) : I(Paper) I(Integer)22c181: Formal Methods in Software Engineering – p.18/33
Operations: QueriesPaperclass mber():Integer{query}attributesoperationname & signatureSemantics of queries (side-effect free operations, aka pure methods)Function from owner and parameter classes to result classOwnerz } {I(getNumber()) : I(Paper) I(Integer)Semantics of static queries omits owner class argument.22c181: Formal Methods in Software Engineering – p.18/33
Operations with Side e()getNumber():Integer{query}class nameattributesoperationname & signature22c181: Formal Methods in Software Engineering – p.19/33
Operations with Side e()getNumber():Integer{query}class nameattributesoperationname & signatureSemantics (operations w/o result)Transition from snapshot to snapshot(relation between sets of snapshots)22c181: Formal Methods in Software Engineering – p.19/33
Operations with Side e()getNumber():Integer{query}class nameattributesoperationname & signatureSemantics (operations w/o result)Transition from snapshot to snapshot(relation between sets of snapshots)We are not more specific for now: only queries allowed in OCL22c181: Formal Methods in Software Engineering – p.19/33
Abstract perLongPaper22c181: Formal Methods in Software Engineering – p.20/33
Abstract perLongPaperSemantics of Abstract Classes (and Interfaces)I(Paper ) I(ShortPaper) I(LongPaper)I(ShortPaper) I(LongPaper) {null}No “direct” elements in I(Paper )22c181: Formal Methods in Software Engineering – p.20/33
Association rks22c181: Formal Methods in Software Engineering – p.21/33
Association rksSemanticsI(Report) is a subset of I(Person)\{null} I(Paper)\{null}22c181: Formal Methods in Software Engineering – p.21/33
Data Types data type Integer (i2:Integer):Boolean (i2:Integer):Integer (i2:Integer):Integer data type String ring2:String):Stringsubstring(lower:Integer, upper:Integer):String22c181: Formal Methods in Software Engineering – p.22/33
Data TypesSyntaxUML stereotype data typeNo attributesSemanticsSemantics I(C) of a data type class C fixed for all snapshots II(Integer) is the same in all snapshotsAll operations are queries (no side effects)I( ) : I(Integer) I(Integer) I(Integer)22c181: Formal Methods in Software Engineering – p.23/33
review*Paperauthors[*]:Personnumber:Integer enumeration MarksReportrecommend:Marksacceptrejectweakly acceptweakly reject22c181: Formal Methods in Software Engineering – p.24/33
review*Paperauthors[*]:Personnumber:Integer enumeration kly acceptweakly rejectSpecial data type: finite number of instances, explicit representationI(Marks) {accept, reject, weakly accept, weakly reject}22c181: Formal Methods in Software Engineering – p.24/33
Aggregationsaggregation iconString*containsLetter*role nameaSemanticsSame (formal) semantics as an associationPragmaticsPart-of relationship, though may be shared with other objects22c181: Formal Methods in Software Engineering – p.25/33
Compositionscomposition le:StringSemanticsSame (formal) semantics as an associationPragmaticsOwned-by, object lifetime controlled by client ( owner)Client multiplicity 0.1 or 122c181: Formal Methods in Software Engineering – p.26/33
Example: The Composite onent)getChild(n:Integer)22c181: Formal Methods in Software Engineering – p.27/33
Use Case Diagrams. . .Means for specifying required user scenarios of a system22c181: Formal Methods in Software Engineering – p.28/33
Use Case Diagrams. . .Means for specifying required user scenarios of a systemKey concepts:ActorRole that user plays wrt system;Car Mechanicoutside the system.22c181: Formal Methods in Software Engineering – p.28/33
Use Case Diagrams. . .Means for specifying required user scenarios of a systemKey concepts:ActorRole that user plays wrt system;Car Mechanicoutside the system.Use CaseSet of scenarios subsumedRepairServiceunder common user goal22c181: Formal Methods in Software Engineering – p.28/33
Use Case Diagrams. . .Means for specifying required user scenarios of a systemKey concepts:ActorRole that user plays wrt system;Car Mechanicoutside the system.Use CaseRepairServiceSet of scenarios subsumedunder common user goalSubjectSystem implementing the use caseWorkshopConnections between use cases, actors and other use cases(stereotypes include and extend )22c181: Formal Methods in Software Engineering – p.28/33
Use Case Syntaxsystem boundary .SystemparticipationUserCreateFileOpenFiledes ece prOpen bynamePrivilegedUser extend Try to opennon-existing filegeneralizationOpen byhyperlink include Browsefile.actoruse case22c181: Formal Methods in Software Engineering – p.29/33
Use Case Relations and StereotypesRelationsParticipation: communication of instances of actor/use caseCan be directed (even towards actor) if communication one-wayGeneralization (actors): communicates with at most as many use casesGeneralization (use cases): more general case22c181: Formal Methods in Software Engineering – p.30/33
Use Case Relations and StereotypesRelationsParticipation: communication of instances of actor/use caseCan be directed (even towards actor) if communication one-wayGeneralization (actors): communicates with at most as many use casesGeneralization (use cases): more general caseStereotypesInclude: behaviour always contains that of included use caseExtend: behaviour can be augmented with that of extending use caseMuch confusion about precise semantics — discouragedPrecedes: user-defined stereotype, not UML standard22c181: Formal Methods in Software Engineering – p.30/33
Use Cases — Important IssuesActors usually persons, but can be also (other) systemUse relations among use cases and among actors with great careDanger: clutter up use cases with detailed analysisDanger: Deal with implementation aspects by extend Use cases can be effective help in requirements analysisUse cases can be bad and confusing “programming language”22c181: Formal Methods in Software Engineering – p.31/33
Sequence DiagramsInteractionScenario realised by system runmechanic: PersonaCar: CaraBulb: BulbcheckBulbsturnOnrepairBulbs22c181: Formal Methods in Software Engineering – p.32/33
Sequence DiagramsInteractionScenario realised by system runLifelineIndividual participant in interaction; instance of class or actormechanic: PersonaCar: CaraBulb: BulbcheckBulbsturnOnrepairBulbs22c181: Formal Methods in Software Engineering – p.32/33
Sequence DiagramsInteractionMessageScenario realised by system runIndividual communication betweenlifelines of interactionLifelineIndividual participant in interaction; instance of class or actormechanic: PersonaCar: CaraBulb: BulbcheckBulbsturnOnrepairBulbs22c181: Formal Methods in Software Engineering – p.32/33
Sequence DiagramsInteractionMessageScenario realised by system runIndividual communication betweenlifelines of interactionLifelineExecution OccurrenceIndividual participant in interaction; instance of class or actormechanic: PersonaCar: CarSegment of lifeline being “active”aBulb: BulbcheckBulbsturnOnrepairBulbs22c181: Formal Methods in Software Engineering – p.32/33
Sequence Diagrams (cont’d)Sequence diagrams model communication in ONE scenarioSequence diagrams refine (part of) ONE use caseDifferent scenarios require different sequence diagramsSequence diagrams are not algorithms!222c181: Formal Methods in Software Engineering – p.33/33
Overview of KeY UML and its semantics Introduction to OCL Specifying requirements with OCL . Vertical proof obligations, using KeY Wrap-up, trends 22c181: Formal Methods in Software Engineering – p.2/33. Building Models 22c181: Formal Methods in Software Engineering – p.3/33. UML
