Jacky, Jonathan; Veanes, Margus; Campbell, Colin; Schulte, Wolfram

Model-Based Software Testing and Analysis with C# : A Model-Based Approach Using Specexplorer

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