Book contents
- Frontmatter
- Contents
- Preface
- Acknowledgments
- I Overview
- II Systems with Finite Models
- 5 Model Programs
- 6 Exploring and Analyzing Finite Model Programs
- 7 Structuring Model Programs with Features and Composition
- 8 Testing Closed Systems
- 9 Further Reading
- III Systems with Complex State
- IV Advanced Topics
- V Appendices
- Bibliography
- Index
6 - Exploring and Analyzing Finite Model Programs
Published online by Cambridge University Press: 02 March 2010
- Frontmatter
- Contents
- Preface
- Acknowledgments
- I Overview
- II Systems with Finite Models
- 5 Model Programs
- 6 Exploring and Analyzing Finite Model Programs
- 7 Structuring Model Programs with Features and Composition
- 8 Testing Closed Systems
- 9 Further Reading
- III Systems with Complex State
- IV Advanced Topics
- V Appendices
- Bibliography
- Index
Summary
In this chapter we introduce exploration our primary technique for analyzing model programs. Exploration generates a finite state machine (FSM) from a model program. The FSM can then be used for visualization, analysis, and offline lest generation.
In this chapter we show how model-based analysis reveals the design errors in the reactive system we discussed in Chapter 3, by exploring the model program we developed in Chapter 5, Section 5.7. We explain and demonstrate safety analysis that identifies unsafe (forbidden) states and liveness analysis that identifies dead states from which goals cannot be reached. Dead states indicate deadlocks (where the program seems to stop running and stops responding to events) or livelocks (where the program keeps running but can't make progress).
In this chapter we also introduce the mpv (Model Program Viewer) tool for visualization and analysis, and explain how to use the modeling library features that support analysis.
Finite state machines
In this section we motivate and explain FSMs.
Simulation is the most limited and labor-intensive model-based analysis technique because it only considers one run at a time (Chapter 5, Section 5.5). To perform more thorough analyses – to detect the design errors discussed in Chapter 3, for example – we need to consider many different runs. The obvious way would be to code a large number of runs, but this is not a practical solution. In order to get good coverage of program behaviors, we would usually have code a great many runs, and some would be very long. But the collection of runs would be redundant. The same sequences of actions would appear again and again in different runs, and even within a single run.
- Type
- Chapter
- Information
- Model-Based Software Testing and Analysis with C# , pp. 94 - 114Publisher: Cambridge University PressPrint publication year: 2007