1©Magee/Kramer 2nd EditionModel Based DesignCSCI 5828: Foundations ofSoftware EngineeringLecture 30Kenneth M. AndersonSlides created by Magee & Kramer for Concurrency TextbookConcurrency: model-based design 2©Magee/Kramer 2nd EditionChapter 8Model-Based DesignConcurrency: model-based design 3©Magee/Kramer 2nd EditionDesignConcepts: design process:requirements to models to implementationsModels: check properties of interest: - safety on the appropriate (sub)system - progress on the overall systemPractice: model interpretation - to infer actual systembehaviorthreads and monitorsAim: rigorous design process.Concurrency: model-based design 4©Magee/Kramer 2nd Edition♦ goals of the system♦ scenarios (Use Case models)♦ properties of interest8.1 from requirements to modelsRequirementsModel♦ identify the main events, actions, and interactions♦ identify and define the main processes♦ identify and define the properties of interest♦ structure the processes into an architecture♦ check traces of interest♦ check properties of interestAnyappropriatedesignapproachcan beused.Concurrency: model-based design 5©Magee/Kramer 2nd Editiona Cruise Control System - requirementsWhen the carignition is switchedon and the onbutton is pressed,the current speedis recorded and thesystem is enabled:it maintains thespeed of the car atthe recordedsetting.Pressing the brake,accelerator or offbutton disables thesystem. Pressingresume or on re-enables the system.buttonsConcurrency: model-based design 6©Magee/Kramer 2nd Editiona Cruise Control System - hardwareWheel revolution sensor generates interrupts to enable the carspeed to be calculated.Parallel Interface Adapter (PIA) is polled every 100msec. Itrecords the actions of the sensors:• buttons (on, off, resume)• brake (pressed)• accelerator (pressed)• engine (on, off).buttonsengineacceleratorbrakePIApolledwheelinterruptCPUthrottleD/AOutput: The cruise control system controls the car speed by settingthe throttle via the digital-to-analogue converter.Concurrency: model-based design 7©Magee/Kramer 2nd Editionmodel - outline design♦outline processes and interactions.Input Speed monitorsthe speed when theengine is on, andprovides the currentspeed readings tospeed control.Sensor Scan monitorsthe buttons, brake,accelerator andengine events.Cruise Controller triggersclear speed and recordspeed, and enables ordisables the speed control.Speed Control clears andrecords the speed, andsets the throttleaccordingly when enabled.Throttlesets theactualthrottle.SensorsPromptsEnginespeedsetThrottleConcurrency: model-based design 8©Magee/Kramer 2nd Editionmodel -design♦ Main events, actions and interactions.on, off, resume, brake, acceleratorengine on, engine off,speed, setThrottleclearSpeed,recordSpeed,enableControl,disableControl♦ Identify main processes.Sensor Scan, Input Speed,Cruise Controller, Speed Control and Throttle♦ Identify main properties.safety - disabled when off, brake or accelerator pressed.♦Define and structure each process.SensorsPromptsConcurrency: model-based design 9©Magee/Kramer 2nd Editionmodel - structure, actions and interactionsset Sensors = {engineOn,engineOff,on,off, resume,brake,accelerator}set Engine = {engineOn,engineOff}set Prompts = {clearSpeed,recordSpeed, enableControl,disableControl}SENSORSCANCRUISECONTROLLERSensorsINPUTSPEEDSPEEDCONTROLsetThrottlespeedEnginePromptsCONTROLCRUISECONTROLSYSTEMTHROTTLETheCONTROLsystem isstructuredas twoprocesses.The mainactions andinteractionsare asshown.Concurrency: model-based design 10©Magee/Kramer 2nd Editionmodel elaboration - process definitionsSENSORSCAN = ({Sensors} -> SENSORSCAN).// monitor speed when engine onINPUTSPEED = (engineOn -> CHECKSPEED),CHECKSPEED = (speed -> CHECKSPEED |engineOff -> INPUTSPEED ).// zoom when throttle setTHROTTLE =(setThrottle -> zoom -> THROTTLE).// perform speed control when enabledSPEEDCONTROL = DISABLED,DISABLED =({speed,clearSpeed,recordSpeed}->DISABLED | enableControl -> ENABLED ),ENABLED = ( speed -> setThrottle -> ENABLED |{recordSpeed,enableControl} -> ENABLED | disableControl -> DISABLED ).Concurrency: model-based design 11©Magee/Kramer 2nd Editionmodel elaboration - process definitionsset DisableActions = {off,brake,accelerator}// enable speed control when cruising, disable when a disable action occursCRUISECONTROLLER = INACTIVE,INACTIVE =(engineOn -> clearSpeed -> ACTIVE |DisableActions -> INACTIVE ),ACTIVE =(engineOff -> INACTIVE |on->recordSpeed->enableControl->CRUISING |DisableActions -> ACTIVE ),CRUISING =(engineOff -> INACTIVE |DisableActions->disableControl->STANDBY |on->recordSpeed->enableControl->CRUISING ),STANDBY =(engineOff -> INACTIVE |resume -> enableControl -> CRUISING |on->recordSpeed->enableControl->CRUISING |DisableActions -> STANDBY ).Concurrency: model-based design 12©Magee/Kramer 2nd Editionmodel - CONTROL subsystem||CONTROL =(CRUISECONTROLLER ||SPEEDCONTROL ).- Is control enabledafter the engine isswitched on and theon button is pressed?- Is control disabledwhen the brake isthen pressed?- Is control re-enabled when resumeis then pressed?Animate to check particulartraces:• Safety: Is the controldisabled when off,brake or acceleratoris pressed?• Progress: Can everyaction eventually beselected?However, we need analysisto check exhaustively :Concurrency: model-based design 13©Magee/Kramer 2nd Editionmodel - Safety propertiesSafety properties should be composed with theappropriate system or subsystem to which theproperty refers. In order that the property can checkthe actions in its alphabet, these actions must not behidden in the system.Safety checks are compositional. If there is no violationat a subsystem level, then there cannot be a violationwhen the subsystem is composed with other subsystems.This is because, if the ERROR state of a particular safetyproperty is unreachable in the LTS of the subsystem, itremains unreachable in any subsequent parallelcomposition which includes the subsystem. Hence...Concurrency: model-based design 14©Magee/Kramer 2nd Editionmodel - Safety propertiesIs CRUISESAFETY violated?||CONTROL =(CRUISECONTROLLER ||SPEEDCONTROL ||CRUISESAFETY ).property CRUISESAFETY = ({DisableActions,disableControl} -> CRUISESAFETY |{on,resume} -> SAFETYCHECK ),SAFETYCHECK = ({on,resume}
View Full Document
Unlocking...