Truth - A Verification Tool for Distributed Systems
We introduce a tool called Truth which aims to serve as a general platform for the systematic investigation of different design languages, semantic models, and logics for distributed systems. In its current version, Truth supports tableau-based model checking for the full mu-calculus and game-based model checking for the alternation-free fragment. Both operate on finite transition systems, given in terms of CCS processes for which our tool additionally offers interactive visualization and simulation features.
Current activities concentrate on the development of a compiler generator which, given the description of a specification language like CCS, automatically generates a corresponding Truth frontend. More specifically, the syntax and the semantics of the language has to be defined using Meseguer's Rewriting Logic formalism, a unified semantic framework for concurrency. From this definition a compiler is derived which parses a given system specification and computes the corresponding semantic object, such as a labelled transition system. The latter can be processed and analyzed further by Truth.
The Truth homepage is located at http://www-i2.informatik.rwth-aachen.de/Forschung/MCS/Truth/
Place: Information technology, Uppsala University