Multi-Core Model Checking for Lay Man

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:

  1. Creating an execution model of (a part of) the system (a priori or a posteriory)
  2. Explicitly or implicitly (symbolically) exploring all the possible states the model can be in: the state space
  3. Verification of the state space for desired properties/absense of undesired properties
This scheme presents a general approach to model checking. Variations are possible for different scenarios.

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.

Project Details

Related projectsEC-MOAN

Project Plan

In the pipeline.


Blom, S.C.C. and van de Pol, J.C. and Weber, M. (2009) Bridging the Gap between Enumerative and Symbolic Model Checkers. Technical Report TR-CTIT-09-30, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625