by Hongyu Zhang, Jeremy S. Bradbury, James R. Cordy, Juergen Dingel
Abstract
With the growing size and complexity of software systems, software verification and validation (V&V) is becoming increasingly important. Model checking and testing are two of the main V&V methods. In this paper, we present a framework that allows for testing and formal modeling and analysis to be combined. More precisely, we describe a framework for model checking and testing implicit invocation software. The framework includes a new programming language — the Implicit Invocation Language (IIL), and a set of formal rule-based transformation tools that allow automatic generation of executable and formal verification artifacts. We evaluate the framework on several small examples. We hope that our approach will advance the state-of-the-art in V&V for event-based systems. Moreover, we plan on using it to explore the relationship between testing and model checking implicit invocation systems and gain insight into their combined benefits.
Bibliographic Information [Bibtex format]
@inproceedings{ZBCD04,
Author = {Hongyu Zhang AND Jeremy S. Bradbury AND James R. Cordy AND Juergen Dingel},
Booktitle = {Proc. of the International Workshop on Distributed Event-Based Systems (DEBS'04)},
Month = {May},
Pages = {110-115},
Title = {A Transformational Framework for Testing and Model Checking Implicit-Invocation Systems},
Year = {2004}}