PowerPoint PresentationStatecharts – brief overviewSlide 3Slide 4Example – gas stationSlide 6Gas stationSlide 8Slide 9Slide 10Cruise Control System SpecificationsCruise Control (CC) EventsSlide 13Slide 14Slide 15Slide 16What Statecharts are good for?What are the problems?What happened in our systems?Our experienceChallengesDiscussion01/14/19 CS599- Formal Methods in SW Architectures1Marija RakicGreg GaoRoshanak Roshandel01/14/19 CS599- Formal Methods in SW Architectures2Statecharts – brief overview•Clustering and refinementACBagbb)(PdDACBag)(Pdb•States and transitions•Arrow- labeled event and optionally a parenthesized condition•Clustered two events to one•D is an abstraction of A and C•D can be refined to consist of A and C•Zooming in and out of D (in latter A and C are not shown)Provide behavioral description of reactive systemsBDagb01/14/19 CS599- Formal Methods in SW Architectures3Statecharts – brief overview•OrthogonalityABDCabin (G)GEgFmdaY•Y is the orthogonal product of A and D01/14/19 CS599- Formal Methods in SW Architectures4Gas Station Specifications1. There will be four pumps at the gas station, and a unique number will identify each pump.2. All pumps are “self serve.”3. Each pump has three nozzles for different type of gas—regular, plus, and premium—denoting different octane content in the gasoline. The prices for the three types of gas vary.4. Each pump has one meter. At any one time, only one person can use one pump.5. All pumps are connected to common storage tanks, one for each of the three types of gas. When the level of gas in a storage tank gets below a set threshold, a request for a refill is issued to an external system.6. It is possible for a customer to pump gas during storage tank refill.7. A customer must pay first. The single gas station attendant accepts cash only.8. Upon payment, the attendant enables a given pump to dispense the paid-for amount of gas.9. The customer can change the decision on the type of gas (s)he wants to fill before starting to fill. Once the customer has started to fill, then the decision cannot be changed.10. Should the customer pre-pay more than (s)he spent to fill the car tank, the gas station attendant will return to the customer his/her change.11. The pump nozzle has a sensor that stops the gas flow once the tank is full.12. The system should handle race conditions, such as a. one customer paying while, in the meantime, another beginning to pump gas at the paid-for pump, andb. one customer beginning to pump at a pump without paying, before another is able to retrieve his/her change.01/14/19 CS599- Formal Methods in SW Architectures5Example – gas stationEvents •“regular”, “premium” or “plus” selected•Level of gas reached threshold•Pump gas•Tank full•Pay•Change picked upAssumptions•The threshold is set in such a way that there is enough gas for the current vehicles on all pumps to finish filling01/14/19 CS599- Formal Methods in SW Architectures6PumpsPump 1Pump 4Pump 3Pump 2StationRefinementClustering01/14/19 CS599- Formal Methods in SW Architectures7Gas stationReady to fi llPump paid f orpay (amount)Enable pumpf or fi llingsame customer at the pumpselect gradeHandling the raise conditionPump i (i=1,2,3,4)I dleReady to fi llFillingstartedFilling donePickupchangepay (amount)nozzle pressedtank f ullnozzle in place(changeexists)nozzle in place(no change)money spentchange pickedGradeselectedselect gradeCheckpointgas above thresholdWaiting f orstation refi llgas below thresholdgas level above threshold01/14/19 CS599- Formal Methods in SW Architectures8Gas station statePump stateI dlePump ready tofi llFilling startedFilling donePickup changepay (in Enough gas)nozzle pressedtank f ullchangeexistsGradeselectedselect grademoney spentnochangechange pickedEnough gas on the stationGas level below thresholdsignal gas belowthreshold/ send request f or refi llsignal gasabovethreshold01/14/19 CS599- Formal Methods in SW Architectures9Grade selectedRegular typeof gasselectedPlus type ofgas selectedPremium typeof gasselectedpremium pressedplus pressedregular pressedReady to fi llFilling startedpremium pressedpremium pressedregular pressed regular pressedplus pressedplus pressednozzle pressednozzle pressednozzle pressednozzlepressed01/14/19 CS599- Formal Methods in SW Architectures10Cruise Control System01/14/19 CS599- Formal Methods in SW Architectures11Cruise Control System Specifications1. You can assume an automatic transmission vehicle.2. For any of the cruise control (CC) functions to take effect, CC must be turned on first.3. CC can be in the following states: off, enabled (i.e., on and cruising), and disabled (on, but not cruising).4. The CC system should be automatically disabled below 30mph and above 90mph.5. Four actions are permitted during CC: set speed, accelerate, decelerate, andresume speed.6. When the system is under CC and the brake is pressed, CC is disabled. When the resume button is pressed, the system resumes at the last set CC speed.7. When the system is under CC and the accelerator pedal is pressed, CC is disabled and the speed increases correspondingly. When the accelerator is released, the CC resumes at its last set CC speed. If at any point of time during acceleration the CC speed is set, CC replaces the old set speed with the new speed.8. If CC is enabled and the vehicle starts going uphill or downhill, CC shouldautomatically apply the accelerator or brake to maintain the set speed.01/14/19 CS599- Formal Methods in SW Architectures12Engine onEngine offCC offCC on (+ cruising+ disabled)Set speed (CC is on)AccelerateDecelerateResume CCCruise Control (CC) Events01/14/19 CS599- Formal Methods in SW Architectures13EngineoffEngineonturn on engineturn off engineTop level states: Engine on and engine offEvents to change states: turn on engine, turn off engine RefinementClustering01/14/19 CS599- Formal Methods in SW Architectures14Engine ofEngine onCC off CC onturn on engineturn off enginepush CC offpush CC onZoom in engine on: CC on and CC offEvents to change states: push CC on, push CC off RefinementClustering01/14/19 CS599- Formal Methods in SW Architectures15CC ofpush CC onCCdisabledCCenabledgas or brake pressedpush CC offresume (sp. already set)pushCC onpushCC offset(curr. sp>30AND curr.sp<90)CConaccelator released(sp. already set)Zoom in CC on: CC enabled and CC disabledDisable to enable: push resume (speed set);
View Full Document
Unlocking...