ABSTRACT

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/

ASTEC seminar

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

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.