© University of Colorado, 2010Model-Based Approach to Designing Concurrent Systems (Part One)Kenneth M. AndersonUniversity of Colorado, BoulderCSCI 5828 — Lecture 12 — 02/18/20101Credit Where Credit is DuePortions of these slides drawn from the course materials developed by Jeff Magee and Jeff Kramer for their excellent bookConcurrency: State Models and Java Programming, 2nd Ed.Portions are thus copyright © John Wiley & Sons, Ltd. 20062GoalsReview material from chapters 1, 2 from the optional textbook (Concurrency: State Models and Java Programming by Magee and Kramer)Present a model-based approach to designing concurrent systemsWhat do we mean by model-based software engineering?Examine fundamental approach used in this book:Concepts, Modeling, PracticeFinite State Processes and Labelled Transition Systems3More on the Authors: “The Two Jeffs”Jeff KramerDean of the Faculty of Engineering and Professor of Distributed Computing at the Department of Computing at Imperial College LondonACM Fellow; Editor of IEEE’s Transactions on Software EngineeringWinner of numerous software engineering awards including best paper and outstanding research awardsJeff MageeProfessor at the Department of Computing at Imperial College LondonLong time member of the SE community with more than 70 journal and conference publications!This book is based on their SE research into modeling concurrency over the past 20 years4Ex.: Cruise Control SystemRequirementsControlled by three buttonson, off, resumeWhen ignition is switched on and on button pressed, current speed is recorded and system maintains the speed of the car at the recorded settingPressing the brake, the accelerator, or the off button disables the systemPressing resume re-enables the systemTwo Threads: Engine and ControlIs the system safe?Would testing reveal all errors?How many paths through system?5Models to the Rescue!To answer, we need a model of the concurrent behavior of the system and then we need to analyze itThis is one benefit of models, they focus on one particular aspect of the world and ignore all othersConsider the model on the front of the Concurrency bookThe picture shows a real-world train next to its modelDepending on the model, you can ask certain questions and get answers that reflect the answers you would get if you asked “the real system”6Models to the Rescue!For the train model, you might be able to askWhat color is the train? How long is it? How many cars does it have?But notWhat’s the train’s maximum speed?How does it behave when a car derails?7Models, continuedA model is a simplified representation of the real worldA model airplane, e.g., used in wind tunnels, models only the external shape of the airplaneThe reduction in scale and complexity achieved by modeling allows engineers to analyze properties of the modelThe earliest models were physical (like our model train)modern models tend to be mathematical and analyzed by computers8Models, continuedEngineers use models to gain confidence in the adequacy and validity of a proposed designfocus on an aspect of interest — concurrencycan animate model to visualize a behaviorcan analyze model to verify propertiesModels support hypothesis testingwe make observations and test against our model’s predictionsif predictions match observations, we gain confidence in the model; otherwise, we update model and try again9Models for ConcurrencyWhen modeling concurrencyour book makes use of a type of finite state machine known as a labeled transition system (LTS)LTS == ModelThese machines are described textually with a specification language called finite state processes (FSP)FSP == Specification LanguageUsed to generate an instance of an LTS10Models for ConcurrencyThese machines can be displayed and analyzed by an analysis tool called LTSANote: LTSA requires a Java 2 run time system, version 1.5.0 or laterOn Windows and Mac OS systems, you can run the LTSA tool by double clicking on its jar fileNote: Its not the most intuitive piece of software, but once you “grok it”, it provides all of the advertised functionality11Modeling the Cruise Control SystemWe won’t model the entire systemlets look at a simplified exampleGiven the following specificationCRUISE = (engineOn -> RUNNING),RUNNING = (speed -> RUNNING | engineOFF -> CRUISE).We can generate a finite state machine that looks like this1213LTSA allows us to enter specifications and generate state machines like the ones on the previous slideIt can also be used to “animate” or step through the state machineLets see a demoNote: animation at left shows the problem we encountered before with the cruise control systemLTSALTSA, continuedUsing a modeling tool, like LTSA, allows us to understand the concurrent behaviors of systems like the cruise control system, BEFORE they are implementedThis can save a lot of time and money, as it is typically easier to test and evolve a model's behavior than it is to implement the system in a programming language14Applying Concepts/Models via ProgrammingThe optional textbook uses Java to enable practice of these conceptsJava iswidely available, generally accepted, and portableprovides sound set of concurrency featuresJava is used for all examples, demo programs, and homework exercises in the optional textbook15Summary So FarConceptsWe adopt a model-based approach for the design and construction of concurrent programsModelsfinite state machines to represent concurrent behaviorPracticeBook uses Java for constructing concurrent programsWe will be presenting numerous examples to illustrate concepts, models and demonstration programs16Modeling Sequential ProcessesWe structure complex systems as sets of simpler activitieseach represented as a sequential processProcesses can overlap or be concurrent, so asto reflect the concurrency inherent in the physical worldor to offload time-consuming tasksor to manage communications and/or other devicesDesigning concurrent software can be complex/error proneA rigorous engineering approach is essential17Overall Approach18Concept of a process as a sequence of actionsModel processes as finite state machinesProgram processes as threads in JavaModeling Processes19Models are described using state machinesLabeled Transition System (LTS)Described textually as finite state processes (FSP)They are displayed and analyzed by the LTSA toolSummaryFSP: textual formLTS: data structureLTSA: visualizer and analyzerModeling ProcessesA process is the execution of a
View Full Document
Unlocking...