• 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
     • Similar to, or as an extension of, the plugin available at https://lms.uni-mb.si/ep4s/
  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

return to the spin homepage