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

Termination is the prototypical liveness property. Differently from safety proper-
ties, observing a finite prefix of a program computation does not give any infor-
mation about whether the computation violates or not a liveness property—the
computation must be considered as a whole. For this reason, the techniques for
verifying liveness properties differ from the ones for safety properties. Another
consequence of this fact is that liveness analysis does not substantially benefit
from testing, which is bound to inspecting finite prefixes of program executions.
To the best of our knowledge, all the techniques in literature for deciding liveness
properties of software are purely static.
Concurrency. From the viewpoint of safety properties, concurrent systems are
essentially equivalent to nondeterministic ones. The guarded command language
admits bounded nondeterminism, the kind of nondeterminism of concurrent sys-
tems that have a finite number of threads. In this paper we do not assume
determinism, unless in few parts where the assumption is explicitly stated. In
practice, concurrency and nondeterminism usually means that the runtime sup-
port of the language (the scheduler) can choose the next state among a set of
possible successors. This hinders the effectiveness of testing, which acts only
through program inputs, in steering the behaviour of programs towards errors.
This issues is tackled by combined approaches either by controlling the schedul-
ing or by backtracking. In the first case, the analysis uses some additional inputs
to control the scheduler, in the second case, the analysis stores unvisited states
to analyze them later. Both approaches can be seen as implementations of the
combination techniques discussed in this paper.
Procedures, encapsulation, polymorphism, dynamic dispatch. Thesimplepro-
gramming language that we consider does not offer any constructs for structuring
large-scale programs, such as procedural abstraction, information hiding, type
inheritance, dynamic dispatching, etc. While these constructs are always present
in real software, most of the combined approaches available in literature are es-
sentially interprocedural. The main reason is that interprocedural static analysis
is a notoriously hard problem (testing, on the other hand, is easily performed
both in an intraprocedural and interprocedural fashion). Some recent efforts are
available in literature, which exploit the static/dynamic combination to improve
interprocedural static analysis, and may deserve future attention [13].
Acknowledgements. This work is partially supported by the European Com-
munity under the call FP7-ICT-2009-5 - project acronym PINCETTE, project
number 257647. The authors are solely responsible for the content of this paper.
It does not represent the opinion of the European Community, and the European
Community is not responsible for any use that might be made of data appearing
therein.
References
1. Anand, S., Pasareanu, C.S., Visser, W.: JPF-SE: A Symbolic Execution Exten-
sion to Java pathFinder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS,
vol. 4424, pp. 134-138. Springer, Heidelberg (2007)