PV5 ⊧ SPINanalyses models of multi-threaded applications with different message passing paradigms or shared memory communication

Application domain/field

• Multi-threaded software
• Model checking
• Simulation
• Concurrency

Type of tool

Model checker + simulator

Expected input

• System description
• Properties: can be expressed as system or process invariants (using assertions), as linear temporal logic (LTL) requirements, as Büchi automata, or as omega-regular properties.

Format:

PROMELA

Expected output

It reports on deadlocks, race conditions, different types of incompleteness, unwarranted assumptions about the relative speed of processes, and property violations.

Internals

Spin is a open-source software verification tool for formal verification of multi-threaded software applications. It can be used in four main modes:

• as a simulator, allowing for rapid prototyping with a random, guided, or interactive simulations
• as an exhaustive verifier, capable of rigorously proving the validity of user specified correctness requirements (using partial order reduction theory to optimize the search)
• as proof approximation system that can validate even very large system models with maximal coverage of the state space.
• as a driver for swarm verification (a new form of swarm computing that can exploit cloud networks of arbitrary size), which can make optimal use of large numbers of available compute cores to leverage parallelism and search diversification techniques, which increases the chance of locating defects in very large verification models.

(source: https://spinroot.com/spin/what.html)

Comments

License: BSD 3-clause open source license