The practical use of model checking in software development

The paper presents the result of work that explored the use of model checking, investigated modeling tools, and developed a process for model checking software systems. A prototype tool for visual modeling was developed and helped the research team understand the role of tools, such as SMV, and clarified the steps involved in the model checking process. The paper summarizes the engineering observations made by team members during their model checking work. These observations were refined through the use of simple challenge problems and organized into a process that highlights some of the practical issues associated with model checking software systems.