[I2 logo] [RWTH logo] MOVES: Software Modeling and Verification
(Informatik 2)
Computer Science / RWTH / I2 / Research / MCS / Truth

Truth Homepage


Truth is a Tool for the Verification of Distributed Systems. It is designed in a highly modular way to enable easy modification to support several design notions, semantic models and corresponding logics. The first beta version is available. The latest paper giving an overview of Truth is here.

Recent Improvements

  • Truth now supports game based model checking for the alternation free fragment of the mu-calculus
  • We developed a specification language compiler (SLC) which turns Truth into a generic verification tool for broad range of specification languages
  • We developed a parallel model checking algorithm for the alternation free fragment of the mu-calculus which is implemented in a dedicated Truth-Version running on a cluster of workstations. A brief description of the algorithm can be found here . Please contact me for further information.
  • Getting Truth

    Truth is available for Solaris and for Linux. To run Truth you need the following software packages:

  • daVinci A tool for the visualization of graphs
  • Java(TM) JDK 1.1.1 or higher is freely obtainable, but you need to register.
  • Java(TM) Swing(TM) Swing Components for JAVA. They are freely obtainable, but you need to register.
  • Objectspace A Generic Collection Library for Java Version 3.0 or higher is also free if you register.
  • dotty (graphviz) A tool vor visualization of graphs, similar to davinci. Just used for visualizing game graphs.
  • Furthermore, the Haskell sources are also available. If you want to compile Truth you need the Glasgow Haskell Compiler. We also provide some locally build ghc packages, usually the latest CVS snapshots which may be more out of date but which are already compiled versions of the compilers.

    Click here to get a version of Truth

    Information for local developers

    Overview of Truth

    The latest paper giving an overview of Truth is here. The first version of Truth was implemented by Stephan Tobies during his master thesis as is described in his thesis (in German). A short overview of the system including a small user's guide was then given in this technical report. The system was officially presented in this paper.

    The following image gives an overview of the term model checking as it should be unterstood by the tool Truth in future releases.

    Valid HTML 4.01 Strict! Valid CSS!