|Webmaster||Disclaimer||Last modified: 2002-10-11 15:19 UTC|
MOVES: Software Modeling and Verification
|Computer Science / RWTH / I2 / Research / AG / MCS / SLC|
SLC - The Specification Language Compiler
What is it for?The Specification Language Compiler (SLC) is a front end for our verification tool Truth. With the help of this compiler is easy to develop a verification tool for a given specification formalism. More specifically, the syntax and semantics of the specification language has to be determined 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 further in subsequent analysis and verification phases. As examples we have already formulated (several versions) Milner's CCS and Petri nets.
To get flavour of the descriptions of specification formalisms check the following examples.
How to get the compiler?The compiler and several examples are provided by several tar-balls. Please note however that a new optimised release is available soon.
How to get more information?There is short report describing a previous version of the compiler. For a complete description of the system and its implementation we refer to the master thesis (in German) of Philipp van Hüllen who implemented the compiler.