Kĩ thuật lập trình - Lecture 10: Specifying systems - Intro

Ivan MarsicRutgers UniversityLECTURE 10: Specifying Systems - Intro*TopicsDomains, PhenomenaStates, EventsContext DiagramsSystems and System DescriptionsBasic Formalisms for SpecificationsBoolean LogicFinite State Machines*World, Parts, Phenomena*Example of a Problem Domains*Example of Problem Domains*Example of Problem DomainsSoftware-to-be(1) Tenant(4) List of valid keys(3) Lock(6) Photosensor(7) Light(8) Alarm bell(9) Desktop computer(2) Landlord(3) Key(5) Device preferences(10) Tenant accounts(11) Log of accesses*Definitions A phenomenon is a fact, or object, or occurrence that appears or is perceived to existAn event is an individual happening, occurring at a particular point in timeEvents are indivisible and instantaneousA state is a relation among individual entities and values, which can change over timeIndividuals are in relation if they share a certain characteristicRelationName(Individual1, , Individualn)*EventsEvents take place at transitions between the states*Relations: ExamplesRelation: Neighbors (Person_i, Person_j)Relation:Sandwich (Bread-slice, Ham-slice, Bread-slice)*Example: States of a DVD PlayerState 1: NotPowered (the player is not powered up)State 2: Powered (the player is powered up)State 3: Loaded (a disc is in the tray)State 4: PlayingState 1: NotPoweredEmpty (the player is not powered up and contains no disc)State 2: NotPoweredLoaded (the player is not powered up and a disc is in the tray)State 3: PoweredEmpty (the player is powered up and contains no disc)State 4: PoweredLoaded (the player is powered up and a disc is in the tray)State 5: Playing*Different AbstractionsDVD playerPowerbuttonPlaybuttonDisctrayDVD playerAtomic objectObject composed of parts(Level of detail)*Example: States of a DVD PlayerSystem Part (Object)State RelationsPower button{Off, On}Disc tray{Empty, Loaded}Play button{Off, On}*State VariablesState VariableState RelationsDoor lock{Disarmed, Armed}Light bulb{Unlit, Lit}Counter of failed attempts{0, 1, , maxNumOfAttempts}Auto-lock timer{0, 1, , autoLockInterval}State variable = a physical part or an attribute of an object*Hidden StatesObservable state: apple’s appearanceHidden state: contains a wormGoal:Find the likelihood of different hidden states, for given observable states*States Example: Stock Market2131.011.001.021.011.001.02Stock_1_PriceMarketindexClosedOpenMarketgateStock_1_Shares2131.011.001.02Stock_2_PriceStock_2_Shares( prices & number of shares for all listed stocks )*Defining StatesCountingDown(Timer) = The relation Equals(Timer, ) holds true for  decreasing with timeIdle(Timer) = The relation Equals(Timer, ) holds true for  remaining constant with time*Microstates and Macrostatesx 1x  2xx 1x  2OrderPendingOrderExecutedMicrostates representing the number of offered shares are aggregated:**EventsEvents marking transitions between the states of a trading order:InPreparationPendingExecutedArchivedsubmitmatchedarchiveEventDescriptiontradeCauses transition between stock states Buy, Sell, or HoldsubmitCauses transition between trading-order statesInPreparation  OrderPendingmatchedCauses transition between trading-order statesOrderPending  OrderExecuted*Context Diagram: DVD Playereject (?)startstopejectloadenabledisableenabledisableactivateshut downPower buttonPlay buttonEject buttonDisc trayDisplayactivateshut downnotifynotifyContext diagram symbols:A box with a double stripe is a software-to-be domain(or, machine domain)A box with a single stripe is a designed domainA box with no stripe is a given domain*Context Diagram: Stock TradingSoftware-to-be(Machine)Stock exchangeTraderBankInvestment portfolioith stockTrading order*Problem Decomposition*Machine and Problem DomainSoftware-to-be(The Machine)Problem DomainTheRequirementabProblem DomainTheRequirementabSpecificationDomain propertiesseen by the software-to-beDomain propertiesseen by the requirementRequirementa: specification interface phenomenab: requirement interface phenomena(a)(b)Software-to-be(The Machine)*Boolean Logic*Propositional Logic conjunction (p and q) implication (if p then q) disjunction (p or q) biconditional (p if and only if q) negation (not p) equivalence (p is equivalent to q)Predicate Logic (extends propositional logic with two quantifiers) universal quantification (for all x, P(x)) existential quantification (there exists x, P(x))*Example: From Req’t to Propositions*LabelDeclarative sentence (not necessarily a proposition!)aThe investor can register with the systembThe email address entered by the investor exists in real world cThe email address entered by the investor is external to our websitedThe login ID entered by the investor is uniqueeThe password entered by the investor conforms to the guidelinesfThe investor enters his/her first and last name, and other demographic infogRegistration is successfulhAccount with zero balance is set up for the investorREQ1 represented as a set of propositionsa( email)( id)( pwd) [B(email)  C(email)  D(id)  E(pwd)  g]fg  h*Example: From Req’t to Propositions*LabelPropositions (partial list)mThe action specified by the investor is “buy”nThe investor specified the upper bound of the “buy” priceoThe investor specified the lower bound of the “sell” priceLabelPropositions (they complete the above list)pThe investor requests to place a market orderqThe investor is shown a blank ticket where the trade can be specified (action, symbol, etc.)rThe most recently retrieved indicative price is shown in the currently open order ticketsThe symbol SYM specified by the investor is a valid ticker symboltThe current indicative price that is obtained from the exchangeuThe system executes the tradevThe system calculates the player’s account new balancewThe system issues a confirmation about the outcome of the transactionxThe system archives the transactionREQ2 represented as a set of propositionsp  q  rsy = v  {(n  o)  [(o  p  o  q)  ( IP)(LB  IP  UB)]}z = m  {[n  (VOL  IP  BAL)]  [n  (VOL  UB  BAL)]}y  z  uu  v  w  x*FSM State Transition DiagramunlocklockunlocklockClosedOpenv = (input-key  Valid-keys) i = (input-key  Valid-keys)M = maxNumOfAttemptsivviv10Start2M*FSMs with Outputsunlock / beeplock / beepunlocklockClosedOpenunlock [key  Valid-keys] / beeplock / beepunlocklockClosedOpen(a)(b)