Rapid prototyping of specification language implementations
Martin Leucker, Thomas Noll · 2003
Specification languages such as LOTOS and SDL play an important role in the design and implementation of distributed systems. Their formal syntax and semantics supports the development of compilers and of verification tools. This paper introduces a generic and uniform approach to support such languages in verification tools. We present a compiler generator which, given the description of a specification language, automatically generates a corresponding implementation. More specifically, the syntax and semantics of the specification language has to be defined using J. Meseguer's (1992, 1996) rewriting logic formalism, which is a unified semantic framework for concurrency. From this description, 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. Thus, we propose some kind of "meta-prototyping" approach, in the sense that new specification formalisms for distributed systems can easily be tested without the need to develop an implementation by hand.