This book teaches model-based analysis and model-based testing: new ways to write and analyze software specifications and designs, generate test cases, and check the results of test runs. The methods increase the automation in each of these activities, so they can be more timely, more thorough, and (we expect) more effective.