Software systems grow larger every day. Still we do not always know with certainty whether or not they function correctly in all possible situations. Model checking solves this problem in three steps:
LTSmin is a model checker that aims at a generic approach. It can explore the state space (step 2) independent from the language in which the model is written (currently supporting; muCRL, mCRL2 and Promela). Property checking (step 3) is also viewed as a language dependent functionality. This way LTSmin can focus on the real algorithmic challenges in model checking while providing means for comparing and combining different model languages.
In model checking, we encounter tough problems of complex input models that result in very large state spaces (often exponential in size compared to the input size). These problems can not be solved by processor speedups, but have to be tackled with parallelism. Large computing grids or clusters provide one approach that LTS-min currently masters (with MPI). However, there is another (anticipated) trend involving the insides of the computing nodes: the introduction of multiple cores on one processor. And this trend we cannot ignore, because at least for LTSmin mutli-core systems present a new challenge.
The introduction of multi-core algorithms, that offer high parallelism by exploiting the shared memories, is not something new in the model checking community. However, it is also not a finished topic and therefore potential for new discoveries. Moreover, we expect that LTSmin provides an interesting playground for several reasons:
Hence we investigate parallel algorithms. In order to use the aggregated memory of multiple workstations, we investigate distributed algorithms. Non-standard solutions, like using external memory (disk) or specialized hardware (stream processors) are under investigation too.