|Webmaster||Disclaimer||Last modified: 2002-10-11 14:24 UTC|
MOVES: Software Modeling and Verification
|Computer Science / RWTH / I2 / Research / MCS / Truth|
TruthTruth 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.
Truth is available for Solaris and for Linux. To run Truth you need the following software packages:
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.
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.