Implementation and Verification of Implicit-Invocation Systems Using Source Transformation

by Hongyu Zhang, Jeremy S. Bradbury, James R. Cordy, Juergen Dingel

Abstract

In this paper we present a source transformation-based framework to support uniform testing and model checking of implicit-invocation software systems. The framework includes a new domain-specific programming language, the Implicit-Invocation Language (IIL), explicitly designed for directly expressing implicit-invocation software systems, and a set of formal rule-based source transformation tools that allow automatic generation of both executable and formal verification artifacts. We provide details of these transformation tools, evaluate the framework in practice, and discuss the benefits of formal automatic transformation in this context. Our approach is designed not only to advance the state-of-the-art in validating implicit-invocation systems, but also to further explore the use of automated source transformation as a uniform vehicle to assist in the implementation, validation and verification of programming languages and software systems in general.

Bibliographic Information [Bibtex format]

@inproceedings{ZBCD05,
Author = {Hongyu Zhang AND Jeremy S. Bradbury AND James R. Cordy AND Juergen Dingel},
Booktitle = {Proc. of the 5th International Workshop on Source Code Analysis and Manipulation (SCAM 2005)},
Month = {Sept./Oct.},
Pages = {87-96},
Title = {Implementation and Verification of Implicit-Invocation Systems Using Source Transformation},
Year = {2005}}

Paper: [PDF]