Details

Autor(en) / Beteiligte

• Holzmann, Gerard J.
• Zelkowitz, Marvin

Titel

Software Model Checking with Spin

Ist Teil von

• Advances In Computers, 2005, Vol.65, p.77-108

Ort / Verlag

United States: Elsevier Science & Technology

Erscheinungsjahr

2005

Beschreibungen/Notizen

• The aim of this chapter is to give an overview of the theoretical foundation and the practical application of logic model checking techniques for the verification of multi-threaded software (rather than hardware) systems. The treatment is focused on the logic model checker Spin, which was designed for this specific domain of application. Spin implements an automata-theoretic method of verification. Although the tool has been available for over 15 years, it continues to evolve, adopting new optimization strategies from time to time to help it tackle larger verification problems. This chapter explains how the tool works, and which types of software verification problems it is designed to handle.