Modeling and Verification Using UML Statecharts (eBook)

front cover 1
copyright 5
table of contents 8
front matter 10
Preface 10
Acknowledgments 12
What’s on the CD-ROM? 13
body 14
1 Formal Requirements and Finite Automata Overview 14
1.1. Terms 14
1.2. Finite Automata: The Basics 15
1.2.1. The Domain of Discourse (Alphabet) 15
1.2.2. An Input Scenario (String) 16
1.2.3. A Requirement (A Formal Language) 17
1.2.4. A Specification 20
1.3. Regular Expressions 20
1.4. Deterministic Finite Automata and Finite State Diagrams 21
1.4.1. Fully and Partially Specified Deterministic Finite Automata 23
1.4.2. A Computation (a Run) 23
1.4.3. An Object-Oriented Interpretation of a Computation 25
1.4.4. Specifying Requirements Using DFA 26
1.4.5. Practical Issues 27
1.4.6. Regular Requirements 28
1.5. Nondeterministic Finite Automata 28
1.5.1. Specifying Requirements Using NFA 31
1.5.2. NFA “Guessing” 31
1.6. Other Forms of FA 32
1.6.1. Universal-FA 32
1.6.2. Alternating Finite Automata 32
1.6.3. NFA, Universal-FA and AFA with e-Transitions 35
1.6.4. Multitape FA 38
1.7. FA Conversions and Lower Bounds 39
1.7.1. From NFA and Universal-FA to DFA 39
1.7.2. From e-NFA to NFA 44
1.7.3. From Regular Expressions to e-NFA 44
1.7.4. From AFA to NFA or Universal-FA 44
1.8. Operations on Regular Requirements 47
1.9. Succinctness of FA 48
1.10. Specifications as Zipped Requirements 51
1.11. Finite State Machines 52
1.12. Normal Form and Minimization of FA and FSMs 53
2 Statecharts 56
2.1. Transformational vs. Reactive Components 56
2.2. Statecharts in Brief 57
2.3. A Related Tool 58
2.4. Basic Elements of Statecharts 59
2.4.1. States and Transitions 59
2.4.2. Concurrence, or Orthogonality 73
2.4.3. History 80
2.5. Code Generation and Scheduling 85
2.5.1. Hierarchical (Horizontal) Code Generation 86
2.5.2. Vertical Code Generation 89
2.5.3. The StateRover Vanilla Code Generation Style 89
2.5.4. StateRover Code Generation for Concurrent Actions 94
2.5.5. Robust Code Generation 96
2.6. Event-Driven Statecharts, Procedural Statecharts, and Mixed Flowcharts and Statecharts 97
2.7. Flowcharts inside Statecharts: Workflow within Event-Driven Controllers 98
2.8. Nonstandard Elements of Statecharts 100
2.8.1. Sub-statecharts 100
2.8.2. Enumerated Flowchart Visual Switch Polygons 104
2.8.3. Parameterized Events 105
2.8.4. Critical Regions 105
2.8.5. Synchronization States 107
2.8.6. Default Events 107
2.8.7. Local Variables and Methods 107
2.9. Passing Data to a Statechart Controller 108
2.10. JUnit Testing of Statechart Objects 108
2.11. Statecharts vs. Message Sequence Charts and Scenarios 111
2.12. Probabilistic Statecharts 111
2.12.1. Example: Black Box Environment Modeling Using Probabilistic Statecharts 112
3 Academic Specification Languages for Reactive Systems 116
3.1. Natural Language Specifications 117
3.2. Using Specification Languages for Runtime Monitoring 119
3.3. Linear-time Temporal Logic (LTL) 121
3.3.1. Background 121
3.3.2. Informal Syntax and Semantics 121
3.3.3. LTL as a Formal Language Recognizer 125
3.3.4. LTL Tautologies and Recurrence Equations 126
3.3.5. Executing LTL Assertions and the Notion of a Cycle 127
3.3.6. LTL with Real-Time Constraints 129
3.3.7. LTL with Time Series Constraints 131
3.3.8. Past Time LTL 132
3.3.9. Infinite-Sequence Semantics of LTL and Automata 133
3.3.10. LTL Expressive Power and Succinctness 134
3.3.11. From LTL to FA 136
3.3.12. LTL Tools 138
3.3.13. Pros and Cons of Using LTL Variants for REM 141
3.4. Other Formal Specification Languages for Reactive Systems 147
3.4.1. Regular Expressions 147
3.4.2. Interval Temporal Logic 149
3.4.3. Graphical Interval Logic 149
3.4.4. Computation Tree Logic 151
3.4.5. TLCharts 152
4 Using Statechart Assertions for Formal Specification 154
4.1. Statechart Specification Assertions 154
4.1.1. Assertion Statecharts: the Basics 154
4.1.2. Terminal State and Assertions 159
4.1.3. Assertion Actions 159
4.1.4. Separating Assertions from the Statechart Model: Interfaces and Event Mapping 159
4.1.5. Simulating and Testing Assertions 160
4.1.6. Asserting about Time 162
4.1.7. Asserting about States of the Primary 168
4.1.8. Scoping Assertions 171
4.1.9. Nesting Assertions 171
4.1.10. Chaining Assertions 173
4.1.11. Default Events 174
4.1.12. Assertions as Flag Raisers 175
4.1.13. Inverting Deterministic Statechart Assertions 175
4.2. Nondeterministic Statechart Assertions 176
4.2.1. Object-Oriented Informal Semantics for Nondeterministic Statecharts 178
4.2.2. Code Generation and Performance Issues 182
4.2.3. Modeling Past Time 186
4.2.4. Default Events for Nondeterministic Assertions 187
4.2.5. Power Usage: Prioritization 188
4.2.6. Power Usage: Shared Variables 191
4.2.7. Power Usage: Orthogonality within Nondeterministic Assertions 192
4.2.8. Quantification and Nondeterministic Statecharts 193
4.2.9. On Deterministic vs. Nondeterministic Statechart Assertions 196
4.2.10. Making Nondeterministic Assertions Deterministic 202
4.2.11. Debugging Nondeterministic Assertions 205
4.2.12. Inverting Nondeterministic Assertions 206
4.2.13. How Do I Write Nondeterministic Assertions? 208
4.3. Operations on Assertions 209
4.4. Quantified Distributed Assertions 213
4.5. Runtime Recovery for Assertion Violations 215
4.5.1. Performance and Reliability Issues 215
4.6. The Language Dog-Fight: Statechart Assertions vs. LTL and ERE 216
4.6.1. Specification Language Conversion 217
4.6.2. From ERE to Nondeterministic Assertions 221
4.7. Succinctness of Pure Statechart Assertions 222
4.8. Temporal Assertions vs. JML and Java Assertions 224
4.9. Commonly Used Assertions 226
5 Creating and Using Temporal Statechart Assertions 230
5.1. Motivation, or Why Use Temporal Assertions? 230
5.1.1. Look at Them: They’re Doing the Same Thing 231
5.1.2. Verifying Temporal Contracts 231
5.1.3. Assertions as Automated Monitors 232
5.1.4. Assertions as Champion Representatives of Individual Concerns 233
5.1.5. Negative Information 239
5.1.6. Assertions in the Context of Statechart Model Changes 240
5.1.7. Assertion Reuse 241
5.1.8. Nondeterministic Assertions 241
5.1.9. Early Requirement Simulation 241
5.1.10. Requirement Tracking 242
5.2. Applying Assertions: Three Uses 242
5.3. Writing Assertions 243
5.3.1. Positioning: Writing Assertions from a Tester’s Perspective 243
5.3.2. Assertion Types 246
5.3.3. From the Human Mind to Correct Assertion 247
5.3.4. Simulating Assertions 252
5.3.5. Assertion Libraries 253
5.4. Runtime Execution Monitoring— Runtime Verification 256
5.4.1. The Role of Assertions during REM 257
5.4.2. Post-Mortem Verification vs. REM 258
5.5. Runtime Recovery from Requirement Violations 258
5.6. Automatic Test Generation 260
5.7. Execution-Based Model Checking 261
5.7.1. Classical Model Checking 262
5.7.2. Execution-Based Model Checking 264
5.7.3. Black-Box Execution-Based Model Checking 265
5.7.4. White-Box Execution-Based Model Checking 265
5.7.5. White-Box Execution-Based Model Checking = White-Box Test Generation + REM 272
6 Application of Formal Specifications and Runtime Monitoring to the Ballistic Missile Defense Project 274
Introduction 274
6.1. Abstract 275
6.2. Context 276
6.3. Formal Specification and Verification Approach 276
6.3.1. Formal Specification Statecharts 286
6.4. Overall Value 289
6.5. Challenges 291
back matter 292
Appendix TLCharts: Syntax and Semantics 292
A.1. About TLCharts 292
A.2. Syntax 294
A.3. Semantics without Temporal Conditions 295
A.4. Semantics with Temporal Conditions 298
A.5. TLCharts with Overlapping States 302
Bibliographical Notes 308
About the Author 315
Index 316
CD-ROM License Agreement 320