CU-Boulder CSCI 5828 - Model- Based Design (34 pages)

Previewing pages 1, 2, 16, 17, 18, 33, 34 of 34 page document View the full content.
View Full Document

Model- Based Design



Previewing pages 1, 2, 16, 17, 18, 33, 34 of actual document.

View the full content.
View Full Document
View Full Document

Model- Based Design

61 views


Pages:
34
School:
University of Colorado at Boulder
Course:
Csci 5828 - Foundations of Software Engineering
Foundations of Software Engineering Documents
Unformatted text preview:

Concurrency model based design 1 Magee Kramer 2nd Edition Concurrency model based design 2 Magee Kramer 2nd Edition Chapter 8 Model Based Design Concurrency model based design 3 Magee Kramer 2nd Edition Design Concepts design process requirements to models to implementations Models check properties of interest safety on the appropriate sub system progress on the overall system Practice model interpretation to infer actual system threads and monitors behavior Aim rigorous design process Concurrency model based design 4 Magee Kramer 2nd Edition 8 1 from requirements to models Requirements Any appropriate design approach can be used Model Concurrency model based design goals of the system scenarios Use Case models properties of interest 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 interest 5 Magee Kramer 2nd Edition a Cruise Control System requirements When the car ignition is switched on and the on button is pressed the current speed is recorded and the system is enabled it maintains the speed of the car at the recorded setting buttons Concurrency model based design Pressing the brake accelerator or off button disables the system Pressing resume or on reenables the system 6 Magee Kramer 2nd Edition a Cruise Control System hardware Parallel Interface Adapter PIA is polled every 100msec It records the actions of the sensors buttons on off resume buttons brake polled PIA accelerator accelerator pressed CPU engine wheel brake pressed interrupt engine on off D A throttle Wheel revolution sensor generates interrupts to enable the car speed to be calculated Output The cruise control system controls the car speed by setting the throttle via the digital to analogue converter Concurrency model based design 7 Magee Kramer 2nd Edition model outline design outline processes and interactions Sensor Scan monitors the buttons brake accelerator and Sensors engine events Engine Input Speed monitors the speed when the engine is on and provides the current speed readings to speed speed control Concurrency model based design Cruise Controller triggers clear speed and record speed and enables or disables the speed control Prompts Speed Control clears and records the speed and sets the throttle accordingly when enabled Throttle sets the actual throttle setThrottle 8 Magee Kramer 2nd Edition model design Main events actions and interactions on off resume brake accelerator engine on engine off speed setThrottle clearSpeed recordSpeed enableControl disableControl Sensors Prompts Identify main processes Sensor Scan Input Speed Cruise Controller Speed Control and Throttle Identify main properties safety disabled when off brake or accelerator pressed Concurrency design Definemodel based and structure each process 9 Magee Kramer 2nd Edition model structure actions and interactions The CONTROL system is structured as two processes The main actions and interactions are as shown CONTROL SENSOR SCAN Sensors Engine INPUT SPEED CRUISE CONTROLLER CRUISE CONTROL SYSTEM Prompts speed SPEED CONTROL THROTTLE set Throttle set Sensors engineOn engineOff on off resume brake accelerator set Engine engineOn engineOff set Prompts clearSpeed recordSpeed enableControl disableControl Concurrency model based design 10 Magee Kramer 2nd Edition model elaboration process definitions SENSORSCAN Sensors SENSORSCAN monitor speed when engine on INPUTSPEED engineOn CHECKSPEED CHECKSPEED speed CHECKSPEED engineOff INPUTSPEED zoom when throttle set THROTTLE setThrottle zoom THROTTLE perform speed control when enabled SPEEDCONTROL 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 Edition model elaboration process definitions set DisableActions off brake accelerator enable speed control when cruising disable when a disable action occurs CRUISECONTROLLER 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 Edition model CONTROL subsystem CONTROL CRUISECONTROLLER SPEEDCONTROL Animate to check particular traces Is control enabled after the engine is switched on and the on button is pressed Is control disabled when the brake is then pressed Is control re enabled when resume is then pressed Concurrency model based design However we need analysis to check exhaustively Safety Is the control disabled when off brake or accelerator is pressed Progress Can every action eventually be selected 13 Magee Kramer 2nd Edition model Safety properties Safety checks are compositional If there is no violation at a subsystem level then there cannot be a violation when the subsystem is composed with other subsystems This is because if the ERROR state of a particular safety property is unreachable in the LTS of the subsystem it remains unreachable in any subsequent parallel composition which includes the subsystem Hence Safety properties should be composed with the appropriate system or subsystem to which the property refers In order that the property can check the actions in its alphabet these actions must not be hidden in the system Concurrency model based design 14 Magee Kramer 2nd Edition model Safety properties property CRUISESAFETY DisableActions disableControl CRUISESAFETY on resume SAFETYCHECK SAFETYCHECK on resume SAFETYCHECK DisableActions SAFETYACTION disableControl CRUISESAFETY SAFETYACTION disableControl CRUISESAFETY LTS CONTROL CRUISECONTROLLER SPEEDCONTROL CRUISESAFETY Is CRUISESAFETY violated Concurrency model based design 15 Magee Kramer 2nd Edition model Safety properties Safety analysis using LTSA produces the following violation Trace to property violation in CRUISESAFETY engineOn clearSpeed Strange circumstances on recordSpeed If the system is enabled by enableControl switching the engine on and engineOff pressing the on button and then off the engine is switched off it off appears that the control system is not disabled Concurrency


View Full Document

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Model- Based Design and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Model- Based Design and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?