This book presents a powerful new language and methodology for programming complex reactive systems in a scenario-based manner. The language is live sequence charts (LSCs), a multimodal extension of sequence charts and UML's sequence diagrams, used in the past mainly for requirements. The methodology is play-in/play-out, an unusually convenient means for specifying inter-object scenario-based behavior directly from a GUI or an object model diagram, with the surprising ability to execute that behavior, or those requirements, directly. The language and methodology are supported by a fully implemented tool – the Play-Engine – which is attached to the book in CD form. Comments from experts in the field: The design of reactive systems is one of the most challenging problems in computer science. This books starts with a critical insight to explain the difficulty of this problem: there is a fundamental gap between the scenario-based way in which people think about such systems and the state-based way in which these systems are implemented. The book then offers a radical proposal to bridge this gap by means of playing scenarios. Systems can be specified by playing in scenarios and implemented by means of a Play-Engine that plays out scenarios. This idea is carried out and developed, lucidly, formally and playfully, to its fullest. The result is a compelling proposal, accompanied by a prototype software engine, for reactive systems design, which is bound to cause a splash in the software-engineering community. Moshe Y. Vardi, Rice University, Houston, Texas, USA Scenarios are a primary exchange tool in explaining system behavior to others, but their limited expressive power never made them able to fully describe systems, thus limiting their use. The language of Live Sequence Charts (LSCs) presented in this beautifully written book achieves this goal, and the attached Play-Engine software makes these LSCs really come alive. This is undoubtedly a key breakthrough that will start long-awaited and exciting new directions in systems specification, synthesis, and analysis. Gérard Berry, Esterel Technologies and INRIA, Sophia-Antipolis, France The approach of David Harel and Rami Marelly is a fascinating way of combining prototyping techniques with techniques for identifying behavior and user interfaces. Manfred Broy, Technical University of Munich, Germany
Author(s): David Harel, Rami Marelly
Edition: 1
Publisher: Springer
Year: 2003
Language: English
Pages: 398
Part I. Prelude......Page 14
1.1 What Are We Talking About?......Page 16
1.2 What Are We Trying to Do?......Page 19
1.3 What’s in the Book?......Page 20
2.1 Modeling and Code Generation......Page 22
2.2 Requirements......Page 25
2.3 Inter-Object vs. Intra-Object Behavior......Page 27
2.4 Live Sequence Charts (LSCs)......Page 29
2.5 Testing, Verification and Synthesis......Page 30
2.6 The Play-In/Play-Out Approach......Page 34
3.1 The Sample System......Page 38
3.2 Playing In......Page 39
3.3 Playing Out......Page 52
3.4 Using Play-Out for Testing......Page 56
3.5 Transition to Design......Page 57
3.6 Time......Page 59
3.7 Smart Play-Out......Page 60
Part II. Foundations......Page 66
4.1 Application Types......Page 68
4.2 Object Properties......Page 69
4.3 And a Bit More Formally......Page 71
5. The Language: Live Sequence Charts (LSCs)......Page 72
5.1 Constant LSCs......Page 73
5.2 Playing In......Page 75
5.3 The General Play-Out Scheme......Page 78
5.4 Playing Out......Page 81
5.5 Combining Locations and Messages......Page 84
5.6 And a Bit More Formally......Page 86
5.7 Bibliographic Notes......Page 94
6. The Tool: The Play-Engine......Page 96
6.1 Bibliographic Notes......Page 100
Part III. Basic Behavior......Page 102
7.1 Symbolic Scenarios......Page 104
7.2 Enriching the Partial Order......Page 107
7.3 Playing Out......Page 110
7.4 And a Bit More Formally......Page 112
7.5 Bibliographic Notes......Page 116
8.1 Using Implemented Functions......Page 118
8.2 Assignments......Page 121
8.3 Playing Out......Page 124
8.4 And a Bit More Formally......Page 127
9.1 Cold Conditions......Page 132
9.2 Hot Conditions......Page 133
9.3 Playing In......Page 134
9.4 Playing Out......Page 139
9.5 And a Bit More Formally......Page 141
9.6 Bibliographic Notes......Page 145
10.1 The If-Then-Else Construct......Page 146
10.2 Subcharts......Page 147
10.3 Nondeterministic Choice......Page 148
10.4 Playing In......Page 149
10.5 Playing Out......Page 151
10.6 And a Bit More Formally......Page 154
10.7 Bibliographic Notes......Page 159
Part IV. Advanced Behavior: Multiple Charts......Page 160
11.1 Simultaneous Activation of Multiple Charts......Page 162
11.2 Overlapping Charts......Page 167
11.3 And a Bit More Formally......Page 170
12.1 Specifying Test Scenarios......Page 172
12.2 Monitoring LSCs......Page 173
12.3 Recording and Replaying......Page 175
12.4 On-line Testing......Page 177
12.5 Executing and Monitoring LSCs in the Play-Engine......Page 178
12.6 And a Bit More Formally......Page 179
12.7 Bibliographic Notes......Page 184
Part V. Advanced Behavior: Richer Constructs......Page 186
13.1 Using Loops......Page 188
13.2 Playing In......Page 189
13.3 Playing Out......Page 191
13.4 Using Variables Within Loops......Page 192
13.5 Executing and Monitoring Dynamic Loops......Page 194
13.6 And a Bit More Formally......Page 196
13.7 Bibliographic Notes......Page 200
14.1 The Design Phase......Page 202
14.2 Incorporating Internal Objects......Page 203
14.3 Calling Object Methods......Page 206
14.4 Playing Out......Page 209
14.5 External Objects......Page 211
14.6 And a Bit More Formally......Page 214
14.7 Bibliographic Notes......Page 218
15.1 Symbolic Instances......Page 222
15.2 Classes and Objects......Page 223
15.3 Playing with Simple Symbolic Instances......Page 225
15.4 Symbolic Instances in the Main Chart......Page 226
15.5 Quantified Binding......Page 228
15.6 Reusing a Scenario Prefix......Page 229
15.8 An Advanced Example: NetPhone......Page 231
15.9 And a Bit More Formally......Page 233
15.10 Bibliographic Notes......Page 240
16.1 An Example......Page 242
16.2 Adding Time to LSCs......Page 243
16.3 Hot Timing Constraints......Page 244
16.4 Cold Timing Constraints......Page 247
16.5 Time Events......Page 248
16.6 Playing In......Page 249
16.7 Playing Out......Page 250
16.8 Unification of Clock Ticks......Page 252
16.9 The Time-Enriched NetPhone Example......Page 253
16.10 And a Bit More Formally......Page 255
16.11 Bibliographic Notes......Page 260
17.1 Example: A Cruise Control System......Page 264
17.2 Forbidden Messages......Page 265
17.3 Generalized Forbidden Messages......Page 268
17.4 Symbolic Instances in Forbidden Messages......Page 269
17.5 Forbidden Conditions......Page 271
17.6 Scoping Forbidden Elements......Page 275
17.7 Playing Out......Page 277
17.9 A Tolerant Semantics for LSCs......Page 279
17.10 And a Bit More Formally......Page 281
17.11 Bibliographic Notes......Page 291
Part VI. Enhancing the Play-Engine......Page 292
18.1 Introduction......Page 294
18.2 Being Smart Helps......Page 296
18.3 The General Approach......Page 300
18.4 The Translation......Page 302
18.5 Current Limitations......Page 312
18.6 Satisfying Existential Charts......Page 314
18.7 Bibliographic Notes......Page 320
19.1 The Engine’s Environment......Page 322
19.2 Playing In......Page 323
19.3 Playing Out......Page 324
19.5 Additional Play-Engine Features......Page 326
20.1 Who Needs a GUI Editor?......Page 330
20.3 What Does GUIEdit Do?......Page 331
20.4 Incorporating Custom Controls......Page 334
20.6 Bibliographic Notes......Page 335
21.1 Object Refinement and Composition......Page 338
21.2 Object Model Diagrams, Inheritance and Interfaces......Page 340
21.3 Dynamic Creation and Destruction of Objects......Page 341
21.4 Structured Properties and Types......Page 342
21.5 Linking Multiple Engines......Page 343
Part VII. Appendices......Page 346
A.1 System Model and Events......Page 348
A.2 LSC Specification......Page 351
A.3 Operational Semantics......Page 357
B. XML Description of a GUI Application......Page 372
C.1 Visual Basic Code......Page 376
D. The GUI Application Interface......Page 378
D.1 Visual Basic Code......Page 379
E. The Structure of a (Recorded) Run......Page 382
References......Page 384
Index......Page 390
