| Preface | p. xi |
| Acknowledgments | p. xv |
| Overview | |
| Describe, Analyze, Test | p. 3 |
| Model programs | p. 4 |
| Model-based analysis | p. 5 |
| Model-based testing | p. 7 |
| Model programs in the software process | p. 8 |
| Syllabus | p. 11 |
| Why We Need Model-Based Testing | p. 13 |
| Client and server | p. 13 |
| Protocol | p. 14 |
| Sockets | p. 15 |
| Libraries | p. 15 |
| Applications | p. 20 |
| Unit testing | p. 23 |
| Some simple scenarios | p. 25 |
| A more complex scenario | p. 27 |
| Failures in the field | p. 28 |
| Failures explained | p. 29 |
| Lessons learned | p. 29 |
| Model-based testing reveals the defect | p. 30 |
| Exercises | p. 31 |
| Why We Need Model-Based Analysis | p. 32 |
| Reactive system | p. 32 |
| Implementation | p. 34 |
| Unit testing | p. 41 |
| Failures in simulation | p. 44 |
| Design defects | p. 46 |
| Reviews and inspections, static analysis | p. 47 |
| Model-based analysis reveals the design errors | p. 47 |
| Exercises | p. 52 |
| Further Reading | p. 53 |
| Systems with Finite Models | |
| Model Programs | p. 57 |
| States, actions, and behavior | p. 57 |
| Case study: user interface | p. 59 |
| Preliminary analysis | p. 61 |
| Coding the model program | p. 64 |
| Simulation | p. 70 |
| Case study: client/server | p. 72 |
| Case study: reactive program | p. 82 |
| Other languages and tools | p. 92 |
| Exercises | p. 93 |
| Exploring and Analyzing Finite Model Programs | p. 94 |
| Finite state machines | p. 94 |
| Exploration | p. 99 |
| Analysis | p. 106 |
| Exercise | p. 114 |
| Structuring Model Programs with Features and Composition | p. 115 |
| Scenario control | p. 115 |
| Features | p. 117 |
| Composition | p. 121 |
| Choosing among options for scenario control | p. 129 |
| Composition for analysis | p. 131 |
| Exercises | p. 136 |
| Testing Closed Systems | p. 137 |
| Offline test generation | p. 137 |
| Traces and terms | p. 139 |
| Test harness | p. 142 |
| Test execution | p. 146 |
| Limitations of offline testing | p. 147 |
| Exercises | p. 148 |
| Further Reading | p. 150 |
| Systems with Complex State | |
| Modeling Systems with Structured State | p. 155 |
| "Infinite" model programs | p. 155 |
| Types for model programs | p. 157 |
| Compound values | p. 157 |
| Case study: revision control system | p. 169 |
| Exercises | p. 181 |
| Analyzing Systems with Complex State | p. 183 |
| Explorable model programs | p. 183 |
| Pruning techniques | p. 186 |
| Sampling | p. 190 |
| Exercises | p. 190 |
| Testing Systems with Complex State | p. 191 |
| On-the-fly testing | p. 192 |
| Implementation, model and stepper | p. 194 |
| Strategies | p. 199 |
| Coverage-directed strategies | p. 203 |
| Advanced on-the-fly settings | p. 210 |
| Exercises | p. 218 |
| Further Reading | p. 219 |
| Advanced Topics | |
| Compositional Modeling | p. 223 |
| Modeling protocol features | p. 223 |
| Motivating example: a client/server protocol | p. 224 |
| Properties of model program composition | p. 241 |
| Modeling techniques using composition and features | p. 245 |
| Exercises | p. 246 |
| Modeling Objects | p. 247 |
| Instance variables as field maps | p. 247 |
| Creating instances | p. 249 |
| Object IDs and composition | p. 253 |
| Harnessing considerations for objects | p. 254 |
| Abstract values and isomorphic states | p. 256 |
| Exercises | p. 257 |
| Reactive Systems | p. 259 |
| Observable actions | p. 259 |
| Nondeterminism | p. 261 |
| Asynchronous stepping | p. 264 |
| Partial explorability | p. 265 |
| Adaptive on-the-fly testing | p. 268 |
| Partially ordered runs | p. 272 |
| Exercises | p. 274 |
| Further Reading | p. 275 |
| Appendices | |
| Modeling Library Reference | p. 281 |
| Attributes | p. 282 |
| Data types | p. 292 |
| Action terms | p. 306 |
| Command Reference | p. 308 |
| Model program viewer, mpv | p. 308 |
| Offline test generator, otg | p. 311 |
| Conformance tester, ct | p. 312 |
| Glossary | p. 315 |
| Bibliography | p. 333 |
| Index | p. 341 |
| Table of Contents provided by Ingram. All Rights Reserved. |