Using Source Transformation to Test and Model Check Implicit-Invocation Systems (2006)

Content Provider	CiteSeerX
Author	Zhang, Hongyu Bradbury, Jeremy S. Cordy, James R. Dingel, Juergen
Description	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.
File Format	PDF
Language	English
Publisher Date	2006-01-01
Publisher Institution	SPECIAL ISSUE ON SOURCE CODE ANALYSIS AND MANIPULATION, SCIENCE OF COMPUTER PROGRAMMING
Access Restriction	Open
Subject Keyword	Implicit-invocation System Source Transformation Model Check Implicit-invocation System Transformation Tool Implicit-invocation Software System Uniform Testing Formal Rule-based Source Transformation Formal Automatic Transformation Allow Automatic Generation Source Transformation-based Framework Uniform Vehicle Implicit-invocation Language Formal Verification Artifact New Domain-specific Programming Language Model Checking Software System
Content Type	Text
Resource Type	Article