Model Based Approach to Designing Concurrent Systems Part One Kenneth M Anderson University of Colorado Boulder CSCI 5828 Lecture 12 02 18 2010 University of Colorado 2010 1 Credit Where Credit is Due 2 Portions of these slides drawn from the course materials developed by Jeff Magee and Jeff Kramer for their excellent book Concurrency State Models and Java Programming 2nd Ed Portions are thus copyright John Wiley Sons Ltd 2006 Goals Review 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 systems What do we mean by model based software engineering Examine fundamental approach used in this book Concepts Modeling Practice Finite State Processes and Labelled Transition Systems 3 More on the Authors The Two Jeffs Jeff Kramer Dean of the Faculty of Engineering and Professor of Distributed Computing at the Department of Computing at Imperial College London ACM Fellow Editor of IEEE s Transactions on Software Engineering Winner of numerous software engineering awards including best paper and outstanding research awards Jeff Magee Professor at the Department of Computing at Imperial College London Long 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 years 4 Ex Cruise Control System 5 Requirements Controlled by three buttons on off resume Two Threads Engine and Control Is the system safe Would testing reveal all errors How many paths through system When ignition is switched on and on button pressed current speed is recorded and system maintains the speed of the car at the recorded setting Pressing the brake the accelerator or the off button disables the system Pressing resume re enables the system Models to the Rescue To answer we need a model of the concurrent behavior of the system and then we need to analyze it This is one benefit of models they focus on one particular aspect of the world and ignore all others Consider the model on the front of the Concurrency book The picture shows a real world train next to its model Depending on the model you can ask certain questions and get answers that reflect the answers you would get if you asked the real system 6 Models to the Rescue For the train model you might be able to ask What color is the train How long is it How many cars does it have But not What s the train s maximum speed How does it behave when a car derails 7 Models continued A model is a simplified representation of the real world A model airplane e g used in wind tunnels models only the external shape of the airplane The reduction in scale and complexity achieved by modeling allows engineers to analyze properties of the model The earliest models were physical like our model train modern models tend to be mathematical and analyzed by computers 8 Models continued Engineers use models to gain confidence in the adequacy and validity of a proposed design focus on an aspect of interest concurrency can animate model to visualize a behavior can analyze model to verify properties Models support hypothesis testing we make observations and test against our model s predictions if predictions match observations we gain confidence in the model otherwise we update model and try again 9 Models for Concurrency 10 When modeling concurrency our book makes use of a type of finite state machine known as a labeled transition system LTS LTS Model These machines are described textually with a specification language called finite state processes FSP FSP Specification Language Used to generate an instance of an LTS Models for Concurrency 11 These machines can be displayed and analyzed by an analysis tool called LTSA Note LTSA requires a Java 2 run time system version 1 5 0 or later On Windows and Mac OS systems you can run the LTSA tool by double clicking on its jar file Note Its not the most intuitive piece of software but once you grok it it provides all of the advertised functionality Modeling the Cruise Control System 12 We won t model the entire system lets look at a simplified example Given the following specification CRUISE engineOn RUNNING RUNNING speed RUNNING engineOFF CRUISE We can generate a finite state machine that looks like this LTSA LTSA allows us to enter specifications and generate state machines like the ones on the previous slide It can also be used to animate or step through the state machine Lets see a demo Note animation at left shows the problem we encountered before with the cruise control system 13 LTSA continued 14 Using a modeling tool like LTSA allows us to understand the concurrent behaviors of systems like the cruise control system BEFORE they are implemented This 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 language Applying Concepts Models via Programming 15 The optional textbook uses Java to enable practice of these concepts Java is widely available generally accepted and portable provides sound set of concurrency features Java is used for all examples demo programs and homework exercises in the optional textbook Summary So Far Concepts We adopt a model based approach for the design and construction of concurrent programs Models finite state machines to represent concurrent behavior Practice Book uses Java for constructing concurrent programs We will be presenting numerous examples to illustrate concepts models and demonstration programs 16 Modeling Sequential Processes 17 We structure complex systems as sets of simpler activities each represented as a sequential process Processes can overlap or be concurrent so as to reflect the concurrency inherent in the physical world or to offload time consuming tasks or to manage communications and or other devices Designing concurrent software can be complex error prone A rigorous engineering approach is essential Overall Approach Concept of a process as a sequence of actions Model processes as finite state machines Program processes as threads in Java 18 Modeling Processes Models are described using state machines Labeled Transition System LTS Described textually as finite state processes FSP They are displayed and analyzed by the LTSA tool Summary FSP textual form LTS data structure LTSA visualizer and analyzer 19 Modeling Processes 20 A process is the execution of a sequential
View Full Document
Unlocking...