Software Engineering - Lecture 10: Specifying Systems - Anh Dao Nam

SOFTWARE ENGINEERING Lecture 10 Specifying Systems MBA Course Notes Dr. ANH DAO NAM 1 Software Engineering Slides are from Ivan Marsic, Thomas E. Potok and Bryan Wood, modified by Anh Dao Nam Textbooks:
Bruegge & Dutoit: Object-Oriented Software Engineering: Using UML, Patterns and Java, Third Edition, Prentice Hall, 2010.
Miles & Hamilton: Learning UML 2.0, O’Reilly Media, 2006. Interesting source:
Bryan Wood , UML for ODP system specifications, lecture notes
Japanese Association of Healthcare Information System Industry (JAHSI) of a Japanese Hospital Information Reference Enterprise Model European research projects:
e.g. COMBINE - investigating the organisation and process for component- based system development
Industrial Practice
OMG
UML profile for Enterprise Distributed Object Computing (EDOC) 2 Topics Use of UML for ODP system specifications UML State Machine Diagrams
State Activities: Entry, Do, and Exit Activities
Composite States and Nested States
Concurrency UML Object Constraint Language (OCL)
OCL Syntax
OCL Constraints and Contracts 3 Use of UML for ODP system specifications - X.906 | ISO/IEC 19793 A standard covering: • definition of a set of UML profiles for expressing a system specification in terms of ODP viewpoint specifications • relationships between the resultant ODP viewpoint specifications • relationships between a system specification using ODP viewpoint specifications and the OMG • Model Driven Architecture 4 Modelling concepts Interpretation concepts
entity, abstraction, system, architecture Basic modelling concepts
object, action, environment (of an object), interface, activity, location (in space/time) Specification concepts
composition/decomposition (of objects), type (of an ), template, role 5 Modelling concepts Organisational concepts
configuration (of objects), group, domain Properties of systems and objects
transparency, contracts, QoS, policy and prescriptions on behaviour, Naming concepts
Name, identifier, name space,name resolution Behaviour concepts
activity structure, contractual behaviour, causality, binding, dependability 6 Viewpoints Different abstractions of the same system
reflect different concerns
expressed in terms of specific viewpoint concepts and rules (viewpoint languages) based on the foundation modelling concepts A mechanism for dealing with the complexity of distributed systems 7 Viewpoint Specifications Specifications of a system from different viewpoints
related and mutually consistent Using the viewpoint languages and the foundation modelling concepts 8 ODP viewpoint specifications - different concerns System Enterprise Computation Information Technology Engineering 9 The enterprise specification Specifies the roles played by an system in its organisational environment An object model of a social/commercial organisation in terms of:
enterprise objects
communities (of enterprise objects)
objectives
behaviour
roles
processes
policy 10 The information specification Specifies system behaviour abstracted from implementation An object model of the system describing the semantics of information and of information processing in the system in terms of:
information objects
invariant schema - predicates on information objects that must always be true
static schema - state of information objects at some location in time
dynamic schema - allowable state changes of information objects 11 The computational specification Specifies computational structure in terms of units of distribution and portability and their interactions abstracted from the detail of how distribution is accomplished An object model of the system describing the structure of processing in terms of:
computational objects
interfaces: operations supported
invocations: operations invoked
activities: sequences of invocations
computational bindings 12 The engineering specification Specifies the mechanisms and services that provide the distribution transparencies and QoS constraints required by the system An object model of the system describing the infrastructure supporting the computational structure
basic engineering objects
(infrastructure) engineering objects
clusters, capsules, nodes
channels
functions 13 The technology specification Specifies the procurable pieces from which the system is built. An object model of the system
defining the configuration of technology objects and the interfaces between them that comprise the ODP system
identifying conformance points 14 An ODP system specification - object configuration - interactions between objects at interfaces Computational Enterprise- business context - business processes - information - changes to information - constraints Information Engineering - hardware and software components implementing the system Technology - mechanisms and services to provide the required distribution transparencies and QoS constraints. 15 ODP system specifications and UML RM-ODP defines clear and comprehensive concepts and a framework supporting system specification RM-ODP does not define a notation for expressing a system specification UML defines a notation for system specification UML does not define clear and comprehensive concepts and a framework supporting system specification 16 UML Profiles for ODP Viewpoints e.g. We don’t say “this class models Fred” We say “this class maps to this EO, which models Fred” Universe of Discourse (UOD) ODP Viewpoint specification UML Viewpoint model UML notation models “models” (not defined) maps to (through a profile) expresses “expresses” (not explicitly defined) 17 ODP system specifications and the OMG Model Driven Architecture® A system specification that is compliant with the RM- ODP also satisfies the requirements of the MDA®. Specifically: • the enterprise specification is a computation independent model (CIM) • the information, computational and engineering specifications together form a platform independent model (PIM), where clause 8 of the RM-ODP Part 3 defines a virtual machine which is the context for platform independence • the technology specification is a platform specific model (PSM) • the correspondences between the viewpoint specifications express the transformations by means of which one model is derived from another. 18 Who needs the standard? Needed by system specifiers Needed for communication between system specifiers Needed for communication between stakeholders and implementors Needed for a stable business functionality description
independent of technology and technology change Needed for mission critical business systems 19 Sources Japanese Association of Healthcare Information System Industry (JAHSI) of a Japanese Hospital Information Reference Enterprise Model European research projects:
e.g. COMBINE - investigating the organisation and process for component-based system development Industrial Practice OMG
UML profile for Enterprise Distributed Object Computing (EDOC) 20 State Machine Diagram: Basic Notation Delisted Listing planned Traded initial-listing trade bankruptcy, merger, acquisition, States of Stock_i initial state indicated by terminal state indicated by event transition 21 UML Diagrams Differ from FSMs Modularization of states Concurrent behaviors 22 States of Stock_i trade trade trade trade trade trade trade trade Buy SellHold Traded Buy SellHold Listing planned Delisted Delisted Listing planned Traded initial-listing trade bankruptcy, merger, acquisition, composite state 23 States of Stock_i Delisted IPO planned Traded initial-listing trade bankruptcy, acquisition, merger, Traded IPO planned Delisted trade trade trade trade trade trade trade trade Buy SellHold initial- listing bankruptcy, acquisition, merger, IPO = initial public offering composite state nested state 24 State Activities: Entry, Do, and Exit Activities matched archive cancel, reject view trade Executed Archived Cancelled submit data entry InPreparation Pending do: check_price+supply [buy] check_price+demand [sell] States of a Trading Order “do” state activity 25 State Diagram for Controller timer-expired / signal-reset, set numOfAttemps := 0 autoLockInterval -expired / invalid-key [numOfAttemps ≤ maxNumOfAttempts] / signal-failure invalid-key / signal-failure invalid-key [numOfAttemps > maxNumOfAttempts] / sound-alarm Blocked Locked Accepting valid-key / signal-success valid-key / signal-success, set numOfAttemps := 0 Unlocked Note how the object responds differently to the same event (invalid-key in Accepting state), depending on which events preceded it 26 State Diagram for Controller invalid-key [numOfAttemps ≤ maxNumOfAttempts] / signal-failure invalid-key / signal-failure invalid-key [numOfAttemps > maxNumOfAttempts] / sound-alarm autoLockInterval -expired / timer-expired / signal-reset, set numOfAttemps := 0 Blocked Locked Accepting entry: start timer do: countdown valid-key / signal-success valid-key / signal-success Unlocked entry: start timer do: countdown Need “entry” and “do” state activities for countdown timers 27 Problem: States of a Hotel Room make-reservation / arrive / depart / Vacant Occupied Reserved Problem: - but a guest may be occupying the room while it is reserved by a future guest!? - or the room may be vacant while reserved by a future guest!? ⇒ need a notion of time (“timing diagram”) 28 Problem: States of a Hotel Room Vacant Reserved Time [days] Occupied Reserved by guest BC m a k e - r e s e r v a t i o n C a r r i v e C d e p a r t Reserved by guest C A a r r i v e A d e p a r t B m a k e - r e s e r v a t i o n B a r r i v e B d e p a r t S t a t e s 29 Problem: States of a Hotel Room Vacant Reserved Time [days] Occupied Reserved by guest BC m a k e - r e s e r v a t i o n C a r r i v e C d e p a r t Reserved by guest C A a r r i v e A d e p a r t B m a k e - r e s e r v a t i o n B a r r i v e B d e p a r t What state? ♦What if the guest is late? – “Holding” state? ♦What if the room is overbooked? ♦What when it is being cleaned? Issue: state transitions are weird—”Reserved” is a future state but transitioned to by a current event! 30 Problem: States of a Hotel Room Object: Reservation table Object: Room occupancy Vacant Reserved Time [days] Occupied Reserved by guest BC m a k e - r e s e r v a t i o n Reserved by guest C A a r r i v e A d e p a r t B m a k e - r e s e r v a t i o n Available c u r r e n t t i m e SOLUTION: Introduce a new object! r e s e r v e f r e e Objects send messages that change states 31 Problem: States of a Hotel Room Vacant Reserved Time [days] Occupied C a r r i v e C d e p a r t A a r r i v e A d e p a r t B a r r i v e B d e p a r t Available c u r r e n t t i m e Object 2: Reservation table Object 1: Room occupancy We need two objects: One tracks room’s current state (occupancy) and the other its future state (reservation) 32 OCL: Object Constraint Language OCL is used in UML diagrams to
write constraints in class diagrams
guard conditions in state and activity diagrams based on Boolean logic Boolean expressions (“OCL constraints”) used to state facts about elements of UML diagrams The implementation must ensure that the constraints always hold true 33 Basic OCL Types and Operations 34 Type Values Operations Boolean true, false and, or, xor, not, implies, if-then-else Integer 1, 48, −3, 84967, *, +, −, /, abs() Real 0.5, 3.14159265, 1.e+5 *, +, −, /, floor() String 'With more exploration comes more text.' concat(), size(), substring() 34 OCL: Types of Navigation Class_A – attribute1 – attribute2 – (a) Local attribute (b) Directly related class (c) Indirectly related class Class_A Class_B * * assocBA assocAB Class_A Class_B * * Class_C * * assocBA assocAB assocCB assocBC Within Class_A: self.attribute2 Within Class_A: self.assocAB Within Class_A: self.assocAB.assocBC 35 Accessing Collections in OCL 36 OCLNotation Meaning EXAMPLE OPERATIONS ON ALL OCL COLLECTIONS c->size() Returns the number of elements in the collection c. c->isEmpty() Returns true if c has no elements, false otherwise. c1->includesAll(c2) Returns true if every element of c2 is found in c1. c1->excludesAll(c2) Returns true if no element of c2 is found in c1. c->forAll(var | expr) Returns true if the Boolean expression expr true for all elements in c. As an element is being evaluated, it is bound to the variable var, which can be used in expr. This implements universal quantification ∀. c->forAll(var1, var2 | expr) Same as above, except that expr is evaluated for every possible pair of elements from c, including the cases where the pair consists of the same element. c->exists(var | expr) Returns true if there exists at least one element in c for which expr is true. This implements existential quantification ∃. c->isUnique(var | expr) Returns true if expr evaluates to a different value when applied to every element of c. c->select(expr) Returns a collection that contains only the elements of c for which expr is true. EXAMPLE OPERATIONS SPECIFIC TO OCL SETS s1->intersection(s2) Returns the set of the elements found in s1 and also in s2. s1->union(s2) Returns the set of the elements found either s1 or s2. s->excluding(x) Returns the set s without object x. EXAMPLE OPERATION SPECIFIC TO OCL SEQUENCES seq->first() Returns the object that is the first element in the sequence seq. 36 OCL Constraints and Contracts A contract specifies constraints on the class state that must be valid always or at certain times, such as before or after an operation is invoked Three types of constraints in OCL: invariants, preconditions, and postconditions  An invariant must always evaluate to true for all instance objects of a class, regardless of what operation is invoked and in what order
applies to a class attribute  A precondition is a predicate that is checked before an operation is executed
applies to a specific operation; used to validate input parameters  A postcondition is a predicate that must be true after an operation is executed
also applies to a specific operation; describes how the object’s state was changed by an operation 37 Example Constraints (1) Invariant: the maximum allowed number of failed attempts at disarming the lock must be a positive integer
context Controller inv: self.getMaxNumOfAttempts() > 0 Precondition: to execute enterKey() the number of failed attempts must be less than the maximum allowed number
context Controller::enterKey(k : Key) : boolean pre: self.getNumOfAttempts() < self.getMaxNumOfAttempts() 38 Example Constraints (2) The postconditions for enterKey() are
(Poc1) a failed attempt is recorded
(Poc2) if the number of failed attempts reached the maximum allowed, the system blocks and the alarm bell blurts
Reformulate (Poc1) to: (Poc1′) if the key is not element of the set of valid keys, then the counter of failed attempts after exiting from enterKey() must be by one greater than before entering enterKey() context Controller::enterKey(k : Key) : Boolean -- postcondition (Poc1′): post: let allValidKeys : Set = self.checker.validKeys() if allValidKeys.exists(vk | k = vk) then getNumOfAttempts() = getNumOfAttempts()@pre else getNumOfAttempts() = getNumOfAttempts()@pre + 1 -- postcondition (Poc2): post: getNumOfAttempts() >= getMaxNumOfAttempts() implies self.isBlocked() and self.alarmCtrl.isOn() 39 xUnit / JUnit assert_*_() Verification is usually done using the assert_*_() methods that define the expected state and raise errors if the actual state differs Examples:
assertTrue(4 == (2 * 2));
assertEquals(expected, actual);
assertNull(Object object);
etc. 40 TLA+ Specification [closed, unlit] [open, lit] [closed, lit] turnLightOff (?) unlock(valid key) unlock(valid key)lock lock, unlock(invalid key) lock, unlock(invalid key) MAIN CONFUSION: What is this state diagram representing? The state of _what_ object? 41 Q&A 42