For my precious children, Sarit, Hadas, Efrat, Yair and Tamar, with whom playing has always been so much fun. And for my beloved wife Michal, soul-mate, playmate, teammate and partner. (D.H.) For my dear parents, Terry and Aaron Marelly, who taught me how to play. And for my beloved wife and daughters, Tali, Noa and Adi, with whom I enjoy playing each and every day. (R.M.) Preface This book does not tell a story. Instead, it is about stories. Or rather, in technical terms, it is about scenarios. Scenarios of system behavior. It con- centrates on reactive systems, be they software or hardware, or combined computer-embedded systems, including distributed and real-time systems. We propose a different way to program such systems, centered on inter- object scenario-based behavior. The book describes a language, two tech- niques, and a supporting tool. The language is a rather broad extension of live sequence charts (LSCs), the original version of which was proposed in 1998 by W. Damm and the first-listed author of this book. The first of the two techniques, called play-in, is a convenient way to ‘play in’ scenario- based behavior directly from the system’s graphical user interface (GUI). The second technique, play-out, makes it possible to execute, or ‘play out’, the behavior on the GUI as if it were programmed in a conventional intra- object state-based fashion. All this is implemented in full in our tool, the Play-Engine. Thebookcanbeviewedasofferingimprovementsinsomeofthephasesof known system development life cycles, e.g., requirements capture and anal- ysis, prototyping, and testing. However, there is a more radical way to view the book, namely, as proposing an alternative way to program reactivity, which, being based on inter-object scenarios, is a lot closer to how people think about systems and their behavior. We are excited by the apparent potential of this work. However, whether or not it is adopted and becomes really useful, what kinds of systems are the ideas most fitting for, and how we should develop methodologies for large- scale applications, all remain to a large extent open questions. Whatever the case, we hope that the book triggers further research and experimentation. David Harel and Rami Marelly Rehovot, February 2003 Note on the Software The Play-Engine tool is available with the book for free, and the attached CD contains most of the files needed for using the software. However, some of the ideas behind the play-in and play-out methods are patent-pending, and both the relevant intellectual property and the Play-Engine software itself are owned by the Weizmann Institute of Science. In order to ob- tain the remaining parts of the software, please visit the book’s website, www.wisdom.weizmann.ac.il/∼playbook, where you will be asked to sign an appropriate license agreement and to register your details. Areservationisinorderhere:thePlay-Engineisnotacommercialproduct (at least at the time of writing), and should be regarded as a research-level tool.Thus,itsreliabilityandeaseofusearelessthanwhatwouldbeexpected from professional software, and we cannot be held responsible for its perfor- mance. Nevertheless, we will make an effort to correct bugs and to otherwise improve and modify the tool, posting periodical updates on the website. In fact, we have already made some slight changes in the software since the text of the book was finalized a few weeks ago; these are all documented in the User Guide that is attached to the software. We would be very grateful if readers would use the appropriate locations on the website to report any errors, both in the software and in the text of the book. So,pleasedocomeandvisitthesite,signin,download,play,andenjoy... Acknowledgments Our first thanks go to Werner Damm from the University of Oldenburg. His 1997–98 collaboration with the first-listed author — to which he brought both the scientist’s skill and the pragmatist’s insight — yielded the original version of the LSCs language, which turned out to be the crucial prerequisite of our work. A very special thanks goes to Hillel Kugler and Na’aman Kam for being such demanding, yet tolerant users of the Play-Engine. Many of their com- mentsandsuggestionshavefoundtheirwayintothematerialpresentedhere. Hillel’s work on smart play-out (cosupervised by Amir Pnueli) is the most promising follow-up research project related to the topic of this book, and we would like to further thank him for his help in our research on symbolic instances, and for his dedication in the effort of writing Chap. 18. Na’aman alsosuppliedtheexamplesfromtheC.elegansnematodemodelgiveninthat chapter. We received helpful suggestions and insightful comments from several other people during our work. They include Liran Carmel, Sol Efroni, Yael Kfir, Jochen Klose, Yehuda Koren, Anat Maoz, David Peleg, Amir Pnueli, Ehud Shapiro, Gera Weiss and an anonymous referee. ThanksgotoDanBarakforhisworkonconnectingmultiplePlay-Engines (the SEC project) and for helping with the implementation of external ob- jects. Evgeniy Bart and Maksim Frenkel helped develop an early version of GUIEdit. Thefirst-listedauthorwouldalsoliketothanktheVerimagresearchcenter inGrenoble,anditsdirector,JosephSifakis,foragenerouspart-timevisiting position in 2002, during which parts of the book were written. The second-listed author would like to thank Orna Grumberg and Moti Kehat for helping him make the right choices at the right times. Contents Part I. Prelude 1. Introduction .............................................. 3 1.1 What Are We Talking About? ............................ 3 1.2 What Are We Trying to Do? ............................. 6 1.3 What’s in the Book?..................................... 7 2. Setting the Stage ......................................... 9 2.1 Modeling and Code Generation ........................... 9 2.2 Requirements........................................... 12 2.3 Inter-Object vs. Intra-Object Behavior..................... 14 2.4 Live Sequence Charts (LSCs) ............................. 16 2.5 Testing, Verification and Synthesis ........................ 17 2.6 The Play-In/Play-Out Approach .......................... 21 3. An Example-Driven Overview............................. 25 3.1 The Sample System ..................................... 25 3.2 Playing In.............................................. 26 3.3 Playing Out ............................................ 39 3.4 Using Play-Out for Testing ............................... 43 3.5 Transition to Design..................................... 44 3.6 Time .................................................. 46 3.7 Smart Play-Out......................................... 47 Part II. Foundations 4. The Model: Object Systems............................... 55 4.1 Application Types....................................... 55 4.2 Object Properties ....................................... 56 4.3 And a Bit More Formally ... .............................. 58 XIV Contents 5. The Language: Live Sequence Charts (LSCs).............. 59 5.1 Constant LSCs.......................................... 60 5.2 Playing In.............................................. 62 5.3 The General Play-Out Scheme ............................ 65 5.4 Playing Out ............................................ 68 5.5 Combining Locations and Messages........................ 71 5.6 And a Bit More Formally ... .............................. 73 5.7 Bibliographic Notes ..................................... 81 6. The Tool: The Play-Engine ............................... 83 6.1 Bibliographic Notes ..................................... 87 Part III. Basic Behavior 7. Variables and Symbolic Messages ......................... 91 7.1 Symbolic Scenarios ...................................... 91 7.2 Enriching the Partial Order .............................. 94 7.3 Playing Out ............................................ 97 7.4 And a Bit More Formally ... .............................. 99 7.5 Bibliographic Notes ..................................... 103 8. Assignments and Implemented Functions ................. 105 8.1 Using Implemented Functions............................. 105 8.2 Assignments............................................ 108 8.3 Playing Out ............................................ 111 8.4 And a Bit More Formally ... .............................. 114 9. Conditions ................................................ 119 9.1 Cold Conditions......................................... 119 9.2 Hot Conditions ......................................... 120 9.3 Playing In.............................................. 121 9.4 Playing Out ............................................ 126 9.5 And a Bit More Formally ... .............................. 128 9.6 Bibliographic Notes ..................................... 132 10. Branching and Subcharts ................................. 133 10.1 The If-Then-Else Construct .............................. 133 10.2 Subcharts .............................................. 134 10.3 Nondeterministic Choice ................................. 135 10.4 Playing In.............................................. 136 10.5 Playing Out ............................................ 138 Contents XV 10.6 And a Bit More Formally ... .............................. 141 10.7 Bibliographic Notes ..................................... 146 Part IV. Advanced Behavior: Multiple Charts 11. Executing Multiple Charts ................................ 149 11.1 Simultaneous Activation of Multiple Charts ................ 149 11.2 Overlapping Charts ..................................... 154 11.3 And a Bit More Formally ... .............................. 157 12. Testing with Existential Charts ........................... 159 12.1 Specifying Test Scenarios................................. 159 12.2 Monitoring LSCs........................................ 160 12.3 Recording and Replaying................................. 162 12.4 On-line Testing ......................................... 164 12.5 Executing and Monitoring LSCs in the Play-Engine ......... 165 12.6 And a Bit More Formally ... .............................. 166 12.7 Bibliographic Notes ..................................... 171 Part V. Advanced Behavior: Richer Constructs 13. Loops ..................................................... 175 13.1 Using Loops ............................................ 175 13.2 Playing In.............................................. 176 13.3 Playing Out ............................................ 178 13.4 Using Variables Within Loops ............................ 179 13.5 Executing and Monitoring Dynamic Loops ................. 181 13.6 And a Bit More Formally ... .............................. 183 13.7 Bibliographic Notes ..................................... 187 14. Transition to Design ...................................... 189 14.1 The Design Phase ....................................... 189 14.2 Incorporating Internal Objects ............................ 190 14.3 Calling Object Methods.................................. 193 14.4 Playing Out ............................................ 196 14.5 External Objects........................................ 198 14.6 And a Bit More Formally ... .............................. 201 14.7 Bibliographic Notes ..................................... 205