Sample Spin Model Checking Projects

The topics are divided into three categories: relatively straightforward problems,
problems that require more in-depth knowledge, and more advanced
research problems.

• Basic
  1. Add a 'Wizard mode' to Spin or to Xspin
     • prompt the user for choices, and select settings based on the answers
  2. Implement an Uppaal-like GUI for the definition of simple Spin models
     • this has great demo and educational value, and eases the learning curve for new users
       it should allow for visual definition of simple models, that can be
       verified instantly, with graphical feed-back, and good simulation support
     • it need not support the full functionality of the language
       but provide an entry-level capability for first-time users
  3. Add configuration management support to Xspin
     • remembering all settings of a run, similar to the current LTL manager
     • [completed: coming soon with the new iSpin and Spin Version 6]
  4. Create a standalone version of Pan 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. Build an add-on tool to compute synchronous product of multiple never claims
     • [completed: implemented in Spin 6.0]
  2. 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
  3. Integrate the full Xspin functionality into Eclipse
     • Similar to, or as an extension of, the plugin available at http://lms.uni-mb.si/ep4s/
  4. Add XML-based import/export of models/settings/output
  5. Develop an integrated version of Spin, with builtin pan.c
     (not requiring the current separate compilation of each pan.c)
     • using Spin to compute optimized transition tables, and the rest pre-compiled
     • sacrificing some speed (due to the loss of compilation directive) for convenience
     • or, create a standalone, generic version of Pan, reading transition tables produced by Spin
  6. Add support for never-claims (safety properties) in simulation mode
• Advanced
  1. Add support for inline LTL formulae (specified like assertions, i.e., as statements)
     • [completed, implemented in Spin 6.0]
  2. 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'
  3. Allow the model checker to make use of the computational power of GPUs
     • e.g. for incremental hash-computation, or state compression
  4. Improve support for the direct verification of C code
     • 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
  5. 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 should 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
  6. Change the Promela parser to support stronger type checking

Last updated: November 18, 2010.