Truth - A Verification Tool for Distributed Systems

Dr. Thomas Noll
Department of Teleinformatics
Royal Institute of Technology (KTH)


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

ASTEC seminar

Place: Information technology, Uppsala University
Room: 1549
Time: February 15, 2000 at 13.15 - 14 (+ coffee and discussion)

Room is in Building 1 , Floor 5 , room 49
(in the northern part of the building).

Help on how get here and MIC campus drawing.

There will be an extended period for discussions after the seminar nourished by cookies and coffee.

Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 1 hour.

Updated 04-Feb-2000 09:32 by Roland Grönroos
e-mail: info -at-    Location: