zbMATH — the first resource for mathematics

Rewriting logic as a framework for generic verification tools. (English) Zbl 0962.68080
Futatsugi, Kokichi, The 3rd international workshop on rewriting logic and its applications, RWLW. Kanazawa City Cultural Hall, Kanzawa, Japan, September 18-20, 2000. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 36, 17 p., electronic only (2000).
Summary: We propose to employ rewriting logic as a generic and uniform approach to support different specification languages for distributed systems in verification tools. We present a compiler generator which, given the definition of a language, automatically generates a corresponding model-checking tool. More specifically, the syntax and semantics of the specification language has to be described in terms of rewriting logic, a unified semantic framework for concurrency. From this definition a compiler is derived which is capable of parsing a concrete system specification and of computing the corresponding semantic object, such as a labeled transition system. The compiler is linked together with the existing verification platform TRUTH to obtain a model-checking tool for the specification language in question. As an example we formulate Milner’s CCS, and we conclude by describing the practical results obtained so far and by presenting directions for future work.
For the entire collection see [Zbl 0957.00046].

68Q42 Grammars and rewriting systems
68T27 Logic in artificial intelligence
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: Link