This book teaches new methods for specifying, analyzing, and testing software; essentials for creating high-quality software. These methods increase the automation in each of these steps, making them more timely, more thorough, and more effective. The authors work through several realistic case studies in-depth and detail, using a toolkit built on the C# language and the .NET framework. Readers can also apply the methods in analyzing and testing systems in many other languages and frameworks....
Teaches new methods for specifying, analyzing and testing software that increase automation in each step.
Preface xiAcknowledgments xvOverviewDescribe, Analyze, Test 3Model programs 4Model-based analysis 5Model-based testing 7Model programs in the software process 8Syllabus 11Why We Need Model-Based Testing 13Client and server 13Protocol 14Sockets 15Libraries 15Applications 20Unit testing 23Some simple scenarios 25A more complex scenario 27Failures in the field 28Failures explained 29Lessons learned 29Model-based testing reveals the defect 30Exercises 31Why We Need Model-Based Analysis 32Reactive system 32Implementation 34Unit testing 41Failures in simulation 44Design defects 46Reviews and inspections, static analysis 47Model-based analysis reveals the design errors 47Exercises 52Further Reading 53Systems with Finite ModelsModel Programs 57States, actions, and behavior 57Case study: user interface 59Preliminary analysis 61Coding the model program 64Simulation 70Case study: client/server 72Case study: reactive program 82Other languages and tools 92Exercises 93Exploring and Analyzing Finite Model Programs 94Finite state machines 94Exploration 99Analysis 106Exercise 114Structuring Model Programs with Features and Composition 115Scenario control 115Features 117Composition 121Choosing among options for scenario control 129Composition for analysis 131Exercises 136Testing Closed Systems 137Offline test generation 137Traces and terms 139Test harness 142Test execution 146Limitations of offline testing 147Exercises 148Further Reading 150Systems with Complex StateModeling Systems with Structured State 155"Infinite" model programs 155Types for model programs 157Compound values 157Case study: revision control system 169Exercises 181Analyzing Systems with Complex State 183Explorable model programs 183Pruning techniques 186Sampling 190Exercises 190Testing Systems with Complex State 191On-the-fly testing 192Implementation, model and stepper 194Strategies 199Coverage-directed strategies 203Advanced on-the-fly settings 210Exercises 218Further Reading 219Advanced TopicsCompositional Modeling 223Modeling protocol features 223Motivating example: a client/server protocol 224Properties of model program composition 241Modeling techniques using composition and features 245Exercises 246Modeling Objects 247Instance variables as field maps 247Creating instances 249Object IDs and composition 253Harnessing considerations for objects 254Abstract values and isomorphic states 256Exercises 257Reactive Systems 259Observable actions 259Nondeterminism 261Asynchronous stepping 264Partial explorability 265Adaptive on-the-fly testing 268Partially ordered runs 272Exercises 274Further Reading 275AppendicesModeling Library Reference 281Attributes 282Data types 292Action terms 306Command Reference 308Model program viewer, mpv 308Offline test generator, otg 311Conformance tester, ct 312Glossary 315Bibliography 333Index 341