On the Integration of Software Testing and Formal Analysis - Empirical Software Engineering and Verification - page 157

On the Integration of Software Testing and
Formal Analysis

Pietro Braione, Giovanni Denaro, and Mauro Pezze

Dipartimento di Informatica, Sistemistica e Comunicazione
Universita di Milano-Bicocca
P.zza dell'Ateneo Nuovo, 1
I-20126 Milano, Italy
{ braione,denaro,pezze } @disco.unimib.it

Abstract. The software industry favors dynamic testing over static
analysis of software, because traditional static software analysis tech-
niques do not adequately balance automation, precision and scalability.
Recently several researchers have combined static and dynamic tech-
niques to overcome these problems. Undergoing efforts include concolic
execution, testing-based correctness prove, execution driven abstract in-
terpretation and dynamic invariant generation.
This paper summarizes the state of the art about combining dynamic
testing and static analysis, and designs a roadmap towards a modern
approach to software V&V that enhances dynamic testing with static
analysis techniques. In particular, this paper surveys the most promising
approaches to combine dynamic testing and static program analysis. It
classifies the techniques against a framework of combination patterns,
to facilitate the identification of commonalities and complementarities
between the techniques. It quantifies analytically the gain that stems
from the most important combination patterns. It provides a roadmap
for future research.

1 Introduction

The complexity and ubiquity of current software systems increases the already
high costs of deployed software bugs. This happens in many application do-
mains that span from mass-diffused software, like operating and embedded sys-
tems, to software systems that manage huge investments and human lives, like
e-commerce systems and flight controllers. Current design and development tech-
niques do not adequately match the strict integrity requirements of these sys-
tems, regardless of the effort allocated to detect and remove faults from software
before deployment.
The leading software industry privileges dynamic testing over program anal-
ysis techniques for locating failures and removing faults, because testing scales
better, is effective in exposing many failures with a limited initial effort, and
samples only actual executions, thus avoiding false positives. On the downside,
the ecacy of testing is limited by the fact that testing is based on the observa-
tion of a finite, underapproximating sample of the possible program behaviours,