SPIN model checker

SPIN model checker

SPIN is a general tool for verifying the correctness of distributed software (software design) in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others, and has evolved for more than 15 years. SPIN is an automata-based model checker. Systems to be verified are described in Promela (Process Meta Language), which supports modeling of asynchronous distributed algorithms as non-deterministic automata ("SPIN" stands for "Simple Promela Interpreter"). Properties to be verified are expressed as Linear Temporal Logic (LTL) formulas, which are negated and then converted into Büchi automata as part of the model-checking algorithm. In addition to model-checking, SPIN can also operate as a simulator, following one possible execution path through the system and presenting the resulting execution trace to the user.

Unlike many model-checkers, SPIN does not actually perform model-checking itself, but instead generates C sources for a problem-specific model checker. This rather antique technique saves memory and improves performance, while also allowing the direct insertion of chunks of C code into the model. SPIN also offers a large number of options to further speed up the model-checking process and save memory, such as:
*partial order reduction;
*state compression;
*bitstate hashing (instead of storing whole states, only their hash code is remembered in a bitfield; this saves a lot of memory but voids completeness);
*weak fairness enforcement.

Since 1995, (approximately) annual SPIN workshops have been held for SPIN users, researchers, and those generally interested in model checking. In 2001, the Association for Computing Machinery awarded SPIN its System Software Award.

ee also

* NuSMV

References

*Holzmann, G. J., "The SPIN Model Checker: Primer and Reference Manual". Addison-Wesley, 2004. ISBN 0-321-22862-6.

External links

* [http://www.spinroot.com/ SPIN website]


Wikimedia Foundation. 2010.

Игры ⚽ Нужна курсовая?

Look at other dictionaries:

  • SPIN — (ursprünglich ein Akronym für Simple PROMELA Interpreter) ist eines der bekanntesten Werkzeuge zur Modellprüfung (engl. Model Checking). SPIN prüft endliche Zustandsautomaten (engl. Finite State Machines) mit der temporalen Logik LTL. Zusätzlich… …   Deutsch Wikipedia

  • Spin — may refer to:* Rotation or spin, a movement of an object in a circular motion * Spin (physics) or particle spin, a fundamental property of elementary particles * Spin (flight), a special and often intense case of a stall * Spin (public relations) …   Wikipedia

  • BLAST model checker — The Berkeley Lazy Abstraction Software Verification Tool (BLAST) is a software model checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated… …   Wikipedia

  • Model checking — This article is about checking of models in computer science. For the checking of models in statistics, see regression model validation. In computer science, model checking refers to the following problem: Given a model of a system, test… …   Wikipedia

  • Model Checking — Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d origine informatique ou électronique). Il s agit de vérifier algorithmiquement si un modèle donné, le système lui même ou une… …   Wikipédia en Français

  • Model checking — Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d origine informatique ou électronique). Il s agit de vérifier algorithmiquement si un modèle donné, le système lui même ou une… …   Wikipédia en Français

  • NuSMV — Developer(s) FBK irst (Trento, Italy), CMU (Pittsburgh, PA), The University of Genova (Italy), The University of Trento (Italy) Stable release 2.5.2 / October 29, 2010; 11 months ago (2010 10 29) Written in AN …   Wikipedia

  • Promela — (Process or Protocol Meta Language) is a verification modeling language. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, communication via message channels can be …   Wikipedia

  • Gerard J. Holzmann — (born 1951) is an American computer scientist, best known as the developer of the SPIN model checker.Currently, Holzmann leads the NASA JPL Laboratory for Reliable Software in Pasadena, California. Previously he was at Bell Labs (c1980… …   Wikipedia

  • Rebeca Modeling Language — Rebeca (Reactive Objects Language) is an actor based language with a formal foundation, designed in an effort to bridge the gap between formal verification approaches and real applications. It can be considered as a reference model for concurrent …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”