A transformational framework for testing and model checking implicit-invocation systems

Abstract

With the growing size and complexity of software systems, software verification and validation (V&V) is becoming increasingly important. Model checking and testing aretwo 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 aframework for model checking and testing implicit invocation software. The framework includes a new programming language -- the Implicit Invocation Language (IIL), and aset 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.