Sample Spin Model Checking Projects

Sample Spin Model Checking Projects

Below are projects to extend the Spin model checker. If you have suggestions to be added to the list, or if you're planning to pursue one of these topics, please let us know.
The projects are divided into three categories, depending on the expected level of difficulty.
  • Basic
    1. Add a Wizard Verification Mode to Spin or iSpin
      • prompting the user for choices, and selecting the appropriate settings to run the tool based on the answers
    2. Create a standalone version of Pan.c with support for just the basic exhaustive dfs
      • as an educational tool, for teaching model checking algorithms
      • a similar version could be created for just bitstate search, etc.

  • Intermediate
    1. Develop an algorithm for the simplification of counter-examples (reducing context switches, eliminating irrelevant actions)
      • as an extension of Spin itself, in reading trail files, or
      • as an extension of pan, when writing trail files
    2. Integrate iSpin functionality into Eclipse
    3. Add XML-based import/export of models/settings/counter-examples
    4. Add support for never-claims (safety properties) in Spin random simulations

  • Advanced (PhD-level research projects)
    1. Add support for the use of symbolic values in explicit-state model checking
      • e.g., with a variable taking any value in a specified range, or 'unknown'
    2. Allow the model checker to make use of the computational power of GPUs
      • e.g. for incremental hash-computation, or state compression
    3. Improve support for the direct verification of C code with Modex
      • automatic detection of data that must be tracked, and/or
      • automatic recognition of data that can be excluded from the state vector
      • adding improved support for function calls
    4. Allow processes to die in any order (not just in reverse order of creation)
      • this requires the statevector to be updated by moving data when a 'hole' is created when a process dies
      • it also requires a smarter algorithm for recycling pids
      • possibly, this could be a larger rewrite, where there is not a single flat statevector, but many smaller ones that are combined into the stored vector just before state comparison and storage
    5. Extend the Promela parser to support stronger type checking

Last update: 30 April 2016.

return to the spin homepage